Formalizing the Semantics of Modular DEVS Models with Temporal Logic

MAXIMILIANO CRISTIÁ

París - Francia

Conferencia; Conférence Internationale de Modélisation, Optimisation et Simulation des Systèmes; 2008

Control Theory researchers have been using DEVS models to formalize discrete event systems for a long time \cite{Zeigler00} but, despite such systems are one of the main targets of Software Engineers, the DEVS formalism has not been used and it is hardly known by the formal methods community of Computer Science. This paper is a second attempt to close the gap between these communities by setting the rules to translate modular coupled DEVS models into TLA+ specifications. TLA+ \cite{Lamport00} is a widely known formalism, used by formal methods researchers and practitioners, to specify --hardware or software based-- reactive or concurrent systems. The paper includes the translation into TLA+ of three atomic DEVS models and a modular coupled model, which all together constitute a typical case study.