Simulation of Timed Abstract State Machines with Predicate Logic Model-Checking

摘要

We describe a prototype of a simulator for reactive timed abstract state machines (ASM) that checks whether the generated runs verify a requirements specification represented as a formula of a First Order Timed Logic (FOTL). The simulator deals with ASM w