Article

Analyzing static and temporal properties of simulation models

Author:

Mamadou Kaba TraoréAuthors Info & Claims

WSC '06: Proceedings of the 38th conference on Winter simulation

Pages 897 - 904

Published: 03 December 2006 Publication History

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.

References

[1]

Balci, O. 1998. Verification, Validation, and Accreditation. WSC'98: 42--48.

[2]

Clarke, E., and J. M. Wing. 1996. Formal Methods: State of the Art and Future Directions. ACM Computing Surveys 28 (4). 626--643.

Digital Library

[3]

Davis, P. K., and R. H. Anderson. 2003. Improving the Composability of Department of Defense Models and Simulations. RAND Corporation.

[4]

Friesen, V., A., Nordwig, and M. Weber. 1998. Object-Oriented Specification of Hybrid Systems Using UMLh and ZimOO. ZUM'98: 328--346.

Digital Library

[5]

Graeme, S., and R. Duke. 1992. Specifying Concurrent Systems Using Object-Z. 15th Australian Computer Science Conf.: 1--14.

[6]

Kuhn, D. R., D. Craigen, and M. Saaltink. 2003. Practical Application of Formal Methods in Modeling and Simulation. SCSC'03, Montreal, Canada. July 20--24.

[7]

Lamsweerde, A. V. 2000. Formal Specification: a Roadmap. Conf. on the Future of Software Engineering. 147--159.

Digital Library

[8]

McMillan, K. L. 1992. Symbolic Model Checking. An Approach to the State Explosion Problem. Ph.D. Thesis in Comp. Sc., Carnegie Mellon University.

Digital Library

[9]

Overstreet, C. M., R. E. Nance, and O. Balci. 2002. Issues in Enhancing Model Reuse. Int. Conf. on Grand Challenges for Modeling and Simulation, Jan. 27--31, San Antonio, Texas, USA.

[10]

Paige, R. F. 1997. A Meta-Method for Formal Method Integration. 4th Int. Symposium of Formal Methods Europe. 473--494.

Digital Library

[11]

Saaltink, M. 1997. The Z/EVES system. Lecture Notes in Comp. Sc. 1212. Springer-Verlag: 72--85.

Digital Library

[12]

Sargent, R. G. 2001. Verification and Validation: Some Approaches and Paradigms for Verifying and Validating Simulation Models. WSC'01: 106--114.

Digital Library

[13]

Smith, G. 2000. The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers.

Digital Library

[14]

Spivey, J. M. 1998. The Z Notation: A Reference Manual. 2nd Ed., Prog. Research Group, University of Oxford.

Digital Library

[15]

Stevenson, D. E. 2003. From DEVS to Formal Methods: a Categorical Approach. SCSC'03, Montreal, Canada, 1--6. July 20--24.

[16]

Zeigler, B. P. 1976. Theory of Modelling and Simulation. Wiley & Sons, N.Y.

Digital Library

[17]

Zeigler, B. P. 1984. Multifacetted Modelling and Discrete Event Simulation. Academic Press Inc., London.

Digital Library

[18]

Zeigler, B. P., H. Praehofer, and T. G. Kim. 2000. Theory of Modeling and Simulation. Integrating Discrete Event and Continuous Complex Dynamic Systems. 2nd Ed. Academic Press. Davis.

Digital Library

Cited By

Aliyu HTraoré MBarros FPrähofer HHu XDenil J(2016)Integrated framework for model-driven systems engineeringProceedings of the Symposium on Theory of Modeling & Simulation10.5555/2975389.2975417(1-9)Online publication date: 3-Apr-2016
https://dl.acm.org/doi/10.5555/2975389.2975417
Goldstein RBreslav SKhan ABarros FPrähofer HHu XDenil J(2016)A quantum of continuous simulated timeProceedings of the Symposium on Theory of Modeling & Simulation10.5555/2975389.2975390(1-8)Online publication date: 3-Apr-2016
https://dl.acm.org/doi/10.5555/2975389.2975390
Szabo CTeo Y(2011)An Analysis of the Cost of Validating Semantic ComposabilityProceedings of the 2011 IEEE Workshop on Principles of Advanced and Distributed Simulation10.1109/PADS.2011.5936769(1-8)Online publication date: 14-Jun-2011
https://dl.acm.org/doi/10.1109/PADS.2011.5936769
Show More Cited By

Analyzing static and temporal properties of simulation models
1. Computing methodologies
  1. Modeling and simulation

Recommendations

Graphical scenarios for specifying temporal properties: an automated approach

Temporal logics are commonly used for reasoning about concurrent systems. Model checkers and other finite-state verification techniques allow for automated checking of system model compliance to given temporal properties. These properties are typically ...
Specifying and Monitoring Temporal Properties in Web Services Compositions
ECOWS '09: Proceedings of the 2009 Seventh IEEE European Conference on Web Services

Current Web service composition approaches and languages such as WS-BPEL do not allow to define temporal constraints in a declarative and separate way. Also it is not possible to verify if there are contradictions between the temporal constraints ...
Reasoning about static and dynamic properties in alloy: A purely relational approach

We study a number of restrictions associated with the first-order relational specification language Alloy. The main shortcomings we address are:---the lack of a complete calculus for deduction in Alloy's underlying formalism, the so called relational ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

WSC '06: Proceedings of the 38th conference on Winter simulation

December 2006

2429 pages

ISBN:1424405017

Editors:
L. Felipe Perrone
Bucknell University
,
Barry G. Lawson
University of Richmond
,
Jason Liu
Colorado School of Mines
,
Frederick P. Wieland
Sensis Corporation
,
General Chair:
David Nicol
University of Illinois, Urbana-Champaign
,
Program Chair:
Richard Fujimoto
College of Computing, Georgia Tech

Sponsors

IIE: Institute of Industrial Engineers
ASA: American Statistical Association
IEICE ESS: Institute of Electronics, Information and Communication Engineers, Engineering Sciences Society
IEEE-CS\DATC: The IEEE Computer Society
SIGSIM: ACM Special Interest Group on Simulation and Modeling
NIST: National Institute of Standards and Technology
(SCS): The Society for Modeling and Simulation International
INFORMS-CS: Institute for Operations Research and the Management Sciences-College on Simulation

Publisher

Winter Simulation Conference

Publication History

Published: 03 December 2006

Check for updates

Qualifiers

Article

Conference

WSC06

Sponsor:

IIE
ASA
IEICE ESS
IEEE-CS\DATC
SIGSIM
NIST
(SCS)
INFORMS-CS

WSC06: Winter Simulation Conference 2006

December 3 - 6, 2006

California, Monterey

Acceptance Rates

WSC '06 Paper Acceptance Rate 177 of 252 submissions, 70%;

Overall Acceptance Rate 3,413 of 5,075 submissions, 67%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
136
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Aliyu HTraoré MBarros FPrähofer HHu XDenil J(2016)Integrated framework for model-driven systems engineeringProceedings of the Symposium on Theory of Modeling & Simulation10.5555/2975389.2975417(1-9)Online publication date: 3-Apr-2016
https://dl.acm.org/doi/10.5555/2975389.2975417
Goldstein RBreslav SKhan ABarros FPrähofer HHu XDenil J(2016)A quantum of continuous simulated timeProceedings of the Symposium on Theory of Modeling & Simulation10.5555/2975389.2975390(1-8)Online publication date: 3-Apr-2016
https://dl.acm.org/doi/10.5555/2975389.2975390
Szabo CTeo Y(2011)An Analysis of the Cost of Validating Semantic ComposabilityProceedings of the 2011 IEEE Workshop on Principles of Advanced and Distributed Simulation10.1109/PADS.2011.5936769(1-8)Online publication date: 14-Jun-2011
https://dl.acm.org/doi/10.1109/PADS.2011.5936769
Albert VNketsa ASeguin CMcGraw RImsand EChinni M(2010)Verifying trace inclusion between an experimental frame and a modelProceedings of the 2010 Spring Simulation Multiconference10.1145/1878537.1878688(1-8)Online publication date: 11-Apr-2010
https://dl.acm.org/doi/10.1145/1878537.1878688
Roeder TSchruben L(2010)Information models for queueing system simulationACM Transactions on Modeling and Computer Simulation10.1145/1734222.173422420:2(1-34)Online publication date: 7-May-2010
https://dl.acm.org/doi/10.1145/1734222.1734224
Szabo CTeo YSee SDunkin AIngalls R(2009)A time-based formalism for the validation of semantic composabilityWinter Simulation Conference10.5555/1995456.1995649(1411-1422)Online publication date: 13-Dec-2009
https://dl.acm.org/doi/10.5555/1995456.1995649
Trojet MFrydman CHamri MWainer GShaffer CMcGraw RChinni M(2009)Practical application of "lightweight" Z in DEVS frameworkProceedings of the 2009 Spring Simulation Multiconference10.5555/1639809.1655383(1-8)Online publication date: 22-Mar-2009
https://dl.acm.org/doi/10.5555/1639809.1655383
Szabo CTeo Y(2009)An Approach for Validation of Semantic Composability in Simulation ModelsProceedings of the 2009 ACM/IEEE/SCS 23rd Workshop on Principles of Advanced and Distributed Simulation10.1109/PADS.2009.14(3-10)Online publication date: 22-Jun-2009
https://dl.acm.org/doi/10.1109/PADS.2009.14
Traoré MMolnár SHeath J(2008)SimStudioProceedings of the 1st international conference on Simulation tools and techniques for communications, networks and systems & workshops10.5555/1416222.1416297(1-6)Online publication date: 3-Mar-2008
https://dl.acm.org/doi/10.5555/1416222.1416297

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten