Analyzing Static and Temporal Properties of Simulation Models

This paper shows how a simulation model can be specified so that its static and temporal properties can be formally analyzed. The approach adopted is based on the integration of formal methods (FMs) and the DEVS paradigm. FMs are known to allow symbolic manipulation and reasoning, while DEVS is known as being a well-establish modeling and simulation (M&S) framework. Combining them makes it possible to develop rigorous proofs of the properties of simulation models as regard to design and use requirements. This paper focuses on the so-called atomic specification. Static aspects of the model are captured with the Z formalism, while dynamic aspects are expressed in first order logic. The specification is supported by the Z/EVES tool. A case study is exhibited