Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 14 / Issue 12

available in:   PDF (207 kB) PS (181 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-014-12-1984


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

Anatol Slissenko (University Paris-East, France)

Pavel Vasilyev (University Paris-East, France)

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, model-checking, predicate timed logic, real-time, simulation

Categories: D.2.1, D.2.4