Call for Paper - November 2022 Edition
IJCA solicits original research papers for the November 2022 Edition. Last date of manuscript submission is October 20, 2022. Read More

Safety Design for Simulation Models based on Formal Methods

International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Year of Publication: 2017
Wassim Trojet

Wassim Trojet. Safety Design for Simulation Models based on Formal Methods. International Journal of Computer Applications 180(8):1-5, December 2017. BibTeX

	author = {Wassim Trojet},
	title = {Safety Design for Simulation Models based on Formal Methods},
	journal = {International Journal of Computer Applications},
	issue_date = {December 2017},
	volume = {180},
	number = {8},
	month = {Dec},
	year = {2017},
	issn = {0975-8887},
	pages = {1-5},
	numpages = {5},
	url = {},
	doi = {10.5120/ijca2017916058},
	publisher = {Foundation of Computer Science (FCS), NY, USA},
	address = {New York, USA}


Control theory researchers have been using DEVS models to formalize discrete event systems for a long time. Despite such systems are one of the main targets of Software Engineers, the DEVS formalism lacks tools offering representing and verifying safety properties. The general scope of the paper consists of extending the DEVS framework to support safety properties and verify them by using formal methods. Thus, we offer a possibility for DEVS user to describe safety properties and to verify formally if these properties are preserved during the evolution of the system. We called the extended formalism ”ΦDEVS”. Safety verification is made once a ”ΦDEVS” model is translated to a formal specification using Z notation by performing proof obligation.


  1. B. Zeigler. Theory of Modelling and Simulation. Robert F. Krieger Publishing, 1976.
  2. D. R. Kuhn, D. Craigen, and M. Saaltink. Practical application of formal methods in modeling and simulation. In SCSC’03, 2003.
  3. M. Clarke and M.Wing. Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR), December 1996.
  4. In a Workshop on Model and Simulation Verification and Validation for the 21st Century, Laurel, MD, CD-ROM. The Society for Modeling and Simulation, 2002.
  5. D. R. Kuhn, M. Chandramouli, and R. W. Butler. Cost effective use of formal methods in verification and validation. In Proc. Workshop on Foundations for M&S and V&V in the 21st Century, SCS, San Diego, CA, 2002.
  6. W. Trojet and T. Berradia. System reliability using simulation models and formal methods. International Journal of Computer Applications, 132(17):1–8, December 2015. Published by Foundation of Computer Science (FCS), NY, USA.
  7. L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on software engineering, March 1977.
  8. M. Saaltink. The Z/EVES 2.0 User’s Guide. TR-99-5493-06a. ORA Canada, 1999.
  9. K. Mughwal and R. Rasmussen. A programmer’s guide to Java scjp certification (chapter 6 section 10). Addison wesley, third edition, december 2008.
  10. D. Rosenblum. A practical approach to programming with assertions. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 21, january 1995.


Safety, DEVS, Discrete Event Simulation , Z, Formal Methods, Formal Verification

Learn about the IJCA article correction policy and process
Dealing with any form of infringement.
‘Peer Review – A Critical Inquiry’ by David Shatz
Directly place requests for print/ hard copies of IJCA via Google Docs