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

Anatol Slissenko; Pavel Vasilyev

doi:10.3217/jucs-014-12-1984

JUCS - Journal of Universal Computer Science 14(12): 1984-2006, doi: 10.3217/jucs-014-12-1984

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

Anatol Slissenko^‡, Pavel Vasilyev^‡

‡ University Paris-East, Paris, France

Corresponding author: Anatol Slissenko ( slissenko@univ-paris12.fr )

This article is freely available under the J.UCS Open Content License.

Citation: Slissenko A, Vasilyev P (2008) Simulation of Timed Abstract State Machines with Predicate Logic Model-Checking. JUCS - Journal of Universal Computer Science 14(12): 1984-2006. https://doi.org/10.3217/jucs-014-12-1984

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.

Keywords

abstract state machine, real-time, simulation, predicate timed logic, model-checking