Abstract

The general scope of the paper consists of improving the verification of simulation models through the integration of formal methods. We offer a formal verification approach of DEVS models based on Z notation. DEVS is a formalism that allows the description and analysis of the behavior of discrete event systems, i.e., systems whose state change depends on the occurrence of an event. A DEVS model is essentially validated by the simulation which permits of verifying whether it correctly describes the behavior of the system. However, a simulation does not cover all possible cases that means the model is validated only for the expected behaviors. For this reason, we have integrated the Z formal specification language in the DEVS formalism to detect errors before simulation which is still an important step for the validation. This integration consists of: (1) transforming a DEVS model into an equivalent Z specification and (2) verifying the consistency of the DEVS model on the resulting specification using the tools developed by the Z community. Such consistency is fulfilled by determinism and completeness. Thus, a DEVS model is subjected to an automatic formal verification before proceeding to its simulation.

References

• A. Maria. Introduction to modeling and simulation. In Proceedings of the 1997 Winter Simulation Conference, 1997.
• D. R. Kuhn, D. Craigen, and M. Saaltink. Practical application of formal methods in modeling and simulation. In SCSC’03, 2003.
• M. Clarke and M.Wing. Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR), December 1996.
• B. Zeigler. Theory of Modelling and Simulation. Robert F. Krieger Publishing, 1976.
• M. K. Traor´e. Combining devs and logic. In OICMS, 2005.
• M. K. Traor´e. Analyzing static and temporal properties of simulation models. In Proceedings of the 2006 Winter Simulation Conference, pages 897–904, 2006.
• M. K. Traor´e. Making devs models amenable to formal analysis. In DEVS/HPC/MMS’06, 2006.
• M. Cristia. A tla+ encoding of devs models. In International Modeling and Simulation Multiconference 2007. Buenos Aires, Argentina, 2007.
• M. Cristia. Formalizing the semantics of modular devs models with temporal logic. In 7`eme Conf´erence Internationale de Mod´elisation, Optimisation et Simulation des Syst`emes MOSIM 08. Paris, France, 2008.
• L. Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional, 2002.
• G. P. Hong and T. G. Kim. The devs formalism: A framework for logical analysis and performance evaluation for discrete event systems. IEEE, 1994.
• J. S. Ostroff. Temporal Logic for Real-Time Systems, Advanced Software Development Series. Research Studies Press, 1989.
• S. Lam and A. U. Shankar. Protocol verification via projections. IEEE Transactions on Software Engineering, July 1984.
• B. Zeigler, H. Praehofer, and T. Kim. Theory of Modelling and Simulation. Integrating Discrete Event and Continuous Complex Dynamic Systems. Academic Press, 2000.
• H. S. Song and T. G. Kim. The devs framework for discrete event systems control. In Conference Proceedings AI, Simulation and Planning in High Autonomy Systems, Gainesville, FL, USA, 1994. J. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice-Hall, 1996.
• J. Sun and J. S. Dong. Design synthesis from interaction and state-based specifications. IEEE Transactions on Software Engineering, June 2006.
• M. H. Hwang and B. P. Zeigler. A modular verification framework using finite and deterministic devs. In Proceedings of 2006 DEVS Symposium, Huntsville, AL, USA, 2006.
• M. H. Hwang and B. P. Zeigler. Reachability graph of finite and deterministic devs networks. IEEE Transactions on Automation Science and Engineering, 2009.
• N. Giambiasi, J. L. Paillet, and F. Chaane. From timed automata to devs models. In Proceedings of the 2003 Winter Simulation Conference S. Chick P. J. Sanchez, D. Ferrin, and D. J. Uorrice, 2003.
• S. Burton, J. Clark, A. Galloway, and J. McDermid. Automated v&v for high integrity systems, a targeted formal methods approach. In Proceedings of the 5th NASA Langley Formal Methods Workshop, june 2000.
• M. Saaltink. The Z/EVES 2.0 User’s Guide. TR-99-5493-06a. ORA Canada, 1999.
• K. Mughwal and R. Rasmussen. A programmer’s guide to Java scjp certification (chapter 6 section 10). Addison wesley, third edition, december 2008.
• D. Rosenblum. A practical approach to programming with assertions. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 21, january 1995.
• L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on software engineering, March 1977.
• S. H. Valentine. Putting numbers into the mathematical toolkit. Springer Verlag, pages 9–36, 1993.
• S. H. Valentine. An algebraic introduction of real numbers into z. Harribas, pages 183–204, 1995.