A formal verification approach for DEVS

ABSTRACT

This paper describes several approaches to the formal verification of discrete event systems modeled with the DEVS formalism. We define the operational semantics of the DEVS formalism in terms of a timed transition system, then we characterize a subclass of DEVS models, through the definition of a formalism inspired by DEVS and timed automata, that allows the use of modelchecking tools. Finally, we discuss the application of this tools and present a simple example.

REFERENCES

• 1: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 2: Rajeev Alur , Limor Fix , Thomas A. Henzinger, Event-clock automata: a determinizable class of timed automata, Theoretical Computer Science, v.211 n.1-2, p.253-273, Jan. 28, 1999 [doi>10.1016/S0304-3975(97)00173-4]
• 3: Gerd Behrmann, Alexandre David, and Kim G. Larsen. A tutorial on uppaal. In Marco Bernardo and Flavio Corradini, editors, Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, number 3185 in LNCS, pages 200--236. Springer-Verlag, September 2004.
• 4: H. P. Dacharry and N. Giambiasi. A multi-formalism approach for discrete event system design: a case study. In MOSIM2006 6ème Conférence Francophone de Modélisation et Simulation, 2006.
• 5: Hernán Dacharry and Norbert Giambiasi. Formal verification with timed automata and devs models: a case study. In Proceedings of ASSE'05. Argentine Society for Computer Science and Operational Research, 2005.
• 6: Hernán Dacharry and Norbert Giambiasi. From timed automata to devs models: Formal verification. In Proceedings of SpringSim'05. SCS -- The Society for Modeling and Simulation International, 2005.
• 7: Hernán Dacharry and Norbert Giambiasi. Devsbased timed hierarchy of formalisms. In Proceedings of the International Modeling and Simulation Multiconference 2007 (IMSM07). SCS -- The Society for Modeling and Simulation International, 2007.
• 8: Hernán Dacharry and Norbert Giambiasi. Discrete event modeling through a multi-modeling approach, form a user-oriented perspective. In Proceedings of SpringSim'07. SCS -- The Society for Modeling and Simulation International, 2007.
• 9: Thomas A. Henzinger , Xavier Nicollin , Joseph Sifakis , Sergio Yovine, Symbolic model checking for real-time systems, Information and Computation, v.111 n.2, p.193-244, June 1994 [doi>10.1006/inco.1994.1045]
• 10: Frits W. Vaandrager , Nancy A. Lynch, Action Transducers and Timed Automata, Proceedings of the Third International Conference on Concurrency Theory, p.436-455, August 24-27, 1992
• 11: N. Lynch , F. Vaandrager, FORWARD AND BACKWARD SIMULATIONS PART II: TIMING-BASED SYSTEMS, Massachusetts Institute of Technology, Cambridge, MA, 1995
• 12: Michael Merritt , Francesmary Modugno , Marc R. Tuttle, Time-Constrained Automata (Extended Abstract), Proceedings of the 2nd International Conference on Concurrency Theory, p.408-423, August 26-29, 1991
• 13: Richard E. Nance, The time and state relationships in simulation modeling, Communications of the ACM, v.24 n.4, p.173-179, April 1981 [doi>10.1145/358598.358601]
• 14: Bernard P. Zeigler , Tag Gon Kim , Herbert Praehofer, Theory of Modeling and Simulation, Academic Press, Inc., Orlando, FL, 2000
• 15: Bernard P. Zeigler, Theory of Modelling and Simulation, Krieger Publishing Co., Inc., Melbourne, FL, 1984

INDEX TERMS

Keywords:
DEVS, formal verification, timed automata