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

Abstract

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 with continuous or discrete time. The time constraints are linear inequalities. It can treat two semantics, one with instantaneous actions and another one with delayed actions, the delays being bounded and non-deterministic.