Simulation of Timed Abstract State Machines with Predicate Logic Model-Checking
Дата
Авторы
Slissenko,Anatol
Vasilyev,Pavel
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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.
Ключевые слова
abstract state machine , real-time , simulation , predicate timed logic , model-checking