International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
|
Volume 132 - Issue 17 |
Published: December 2015 |
Authors: Wassim Trojet, Tahar Berradia |
![]() |
Wassim Trojet, Tahar Berradia . System Reliability using Simulation Models and Formal Methods. International Journal of Computer Applications. 132, 17 (December 2015), 1-8. DOI=10.5120/ijca2015907684
@article{ 10.5120/ijca2015907684, author = { Wassim Trojet,Tahar Berradia }, title = { System Reliability using Simulation Models and Formal Methods }, journal = { International Journal of Computer Applications }, year = { 2015 }, volume = { 132 }, number = { 17 }, pages = { 1-8 }, doi = { 10.5120/ijca2015907684 }, publisher = { Foundation of Computer Science (FCS), NY, USA } }
%0 Journal Article %D 2015 %A Wassim Trojet %A Tahar Berradia %T System Reliability using Simulation Models and Formal Methods%T %J International Journal of Computer Applications %V 132 %N 17 %P 1-8 %R 10.5120/ijca2015907684 %I Foundation of Computer Science (FCS), NY, USA
The general scope of the paper consists of improving the verification of simulation models through the integration of formal methods. We offer a formal verification approach of DEVS models based on Z notation. DEVS is a formalism that allows the description and analysis of the behavior of discrete event systems, i.e., systems whose state change depends on the occurrence of an event. A DEVS model is essentially validated by the simulation which permits of verifying whether it correctly describes the behavior of the system. However, a simulation does not cover all possible cases that means the model is validated only for the expected behaviors. For this reason, we have integrated the Z formal specification language in the DEVS formalism to detect errors before simulation which is still an important step for the validation. This integration consists of: (1) transforming a DEVS model into an equivalent Z specification and (2) verifying the consistency of the DEVS model on the resulting specification using the tools developed by the Z community. Such consistency is fulfilled by determinism and completeness. Thus, a DEVS model is subjected to an automatic formal verification before proceeding to its simulation.