Formal and Operational Study of C-DEVS

Abstract

C-DEVS is a formalism for modeling and analysis of discrete event systems. It refers to the original formalism defined by Zeigler in 1976. While the simulation algorithms are well defined, their implementation is a challenge due to both correctness and efficiency issues. This work aims at studying the formalism and its operational semantics. We review and validate the meta-model for SimStudio - a Java implementation of the DEVS simulation protocol, and we debug its existing Java codes. We finally use formal methods to perform model checking and theorem proving on the C-DEVS simulation system to assess the properties of correctness.