Principles of Discrete Event System Specification model verification. (January 2013)

• Record Type: Journal Article
• Authors: Saadawi, Hesham; Wainer, Gabriel
• Other Names: Traoré Mamadou Kaba guest-editor.
• Is Part Of: Simulation. Volume 89:Number 1(2013)
• Page Start: 41
• Page End: 67
• Publication Date: 2013-01
• Subjects: Discrete Event System Specification -- model checking -- Rational Time-Advance Discrete Event System Specification -- real-time systems -- timed automata; Computer simulation -- Periodicals; 003.3
• DOI: 10.1177/0037549711424424
• Languages: English
• ISSNs: 0037-5497

Abstract

Real-time systems modeling and verification is a complex task. In many cases, formal methods have been employed to deal with the complexity of these systems, but checking those models is usually unfeasible. Modeling and simulation methods introduce a means of validating these model's specifications. In particular, Discrete Event System Specification (DEVS) models can be used for this purpose. Here, we introduce a new extension to the DEVS formalism, called the Rational Time-Advance DEVS (RTA-DEVS), which permits modeling the behavior of real-time systems that can be modeled by the classical DEVS; however, RTA-DEVS models can be formally checked with standard model-checking algorithms and tools. In order to do so, we introduce a procedure to create timed automata (TA) models that are behaviorally equivalent to the original RTA-DEVS models. This enables the use of the available TA tools and theories for formal model checking. Further, we introduce a methodology to transform classic DEVS models to RTA-DEVS models, thus enabling formal verification of classic DEVS with an acceptable accuracy.