The week's pick
Random Articles
Reseach Article
Safety Design for Simulation Models based on Formal Methods
| 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
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
- B. Zeigler. Theory of Modelling and Simulation. Robert F. Krieger Publishing, 1976.
- D. R. Kuhn, D. Craigen, and M. Saaltink. Practical application of formal methods in modeling and simulation. In SCSC’03, 2003.
- M. Clarke and M.Wing. Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR), December 1996.
- 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.
- 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.
- 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.
- L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on software engineering, March 1977.
- M. Saaltink. The Z/EVES 2.0 User’s Guide. TR-99-5493-06a. ORA Canada, 1999.
- K. Mughwal and R. Rasmussen. A programmer’s guide to Java scjp certification (chapter 6 section 10). Addison wesley, third edition, december 2008.
- D. Rosenblum. A practical approach to programming with assertions. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 21, january 1995.
Index Terms
Keywords