CFP last date
22 April 2024
Reseach Article

Safety Design for Simulation Models based on Formal Methods

by Wassim Trojet
International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 180 - Number 8
Year of Publication: 2017
Authors: Wassim Trojet
10.5120/ijca2017916058

Wassim Trojet . Safety Design for Simulation Models based on Formal Methods. International Journal of Computer Applications. 180, 8 ( Dec 2017), 1-5. DOI=10.5120/ijca2017916058

@article{ 10.5120/ijca2017916058,
author = { Wassim Trojet },
title = { Safety Design for Simulation Models based on Formal Methods },
journal = { International Journal of Computer Applications },
issue_date = { Dec 2017 },
volume = { 180 },
number = { 8 },
month = { Dec },
year = { 2017 },
issn = { 0975-8887 },
pages = { 1-5 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume180/number8/28817-2017916058/ },
doi = { 10.5120/ijca2017916058 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-07T01:00:03.783020+05:30
%A Wassim Trojet
%T Safety Design for Simulation Models based on Formal Methods
%J International Journal of Computer Applications
%@ 0975-8887
%V 180
%N 8
%P 1-5
%D 2017
%I Foundation of Computer Science (FCS), NY, USA
Abstract

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.

References
  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.
Index Terms

Computer Science
Information Sciences

Keywords

Safety DEVS Discrete Event Simulation Z Formal Methods Formal Verification