Analyzing Static and Temporal Properties of Simulation Models

Author

Traore, Mamadou Kaba

Author_Institution

LIMOS CNRS UNR 6158, Blaise Pascal Univ., Aubiere

fYear

2006

fDate

3-6 Dec. 2006

Firstpage

897

Lastpage

904

Abstract

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

Keywords

digital simulation; formal logic; formal specification; DEVS paradigm; Z formalism; Z/EVES tool; atomic specification; first order logic; formal methods; simulation models; static properties; temporal properties; Accreditation; Analytical models; Flexible manufacturing systems; Logic; Protocols;

fLanguage

English

Publisher

ieee

Conference_Titel

Simulation Conference, 2006. WSC 06. Proceedings of the Winter

Conference_Location

Monterey, CA

Print_ISBN

1-4244-0500-9

Electronic_ISBN

1-4244-0501-7

Type

conf

DOI

10.1109/WSC.2006.323173

Filename

4117697