Formal Verification and Validation of DEVS Simulation Models

We present a model-based verification technique built on selective and pragmatic use of formal methods, by using simplified model checking tools that focus on error detection rather than formalized proofs. This framework is to check and confirm that the trajectories and events of DEVS-Driven Modeling Language (DDML) simulation models and that of the real system agree in order to achieve replicative, predictive and structural validity through the lightweight application of formal methods. This is to reduce and ease the Simulation model verification efforts while increasing the coverage of the process, in order to verify the transformational accuracy of the model development process, increase confidence in the simulation model and allow for performance evaluation of simulation models. This framework provides a model refinement iterative procedure that helps to enhance the DEVS Simulation Model, correct errors or adapt to changing contextual requirements. This refinement procedure is applicable to evolutionary software development and systems requiring rapid prototyping, in order to meet up with changing requirements of such systems with the aid of iterative refinement. Furthermore, we present a case study example of a GSM telecommunication system to reveal the ability of this framework to not only formally verify system but also refine their models.