Guiding Simulation Model Verification by Model Checking

The accuracy and credibility of model is the most important determinant of development of Modeling and Simulation (M&S). There is a desperate need for an immediate practical solution to the problem of VV&A (Validation, Verification and Accreditation) of simulation systems. A discussion and experiment of the relative merits of informal methods and formal methods are provided in this paper. In spite of increasing simulation speed via parallelization, the number of problem cases that can be covered is not highly increased. On the other hand, formal methods have proven to be valuable techniques, but they require detailed specifications of systems and requirements, therefore they are not very accessible in practical simulation systems development. According to the exhaustiveness of formal methods, a Model Driven Architecture (MDA) based simulation VV&A framework guided by model checking is presented in this paper. This framework combines scalability of simulation with exhaustiveness of formal methods in order to get the best of both worlds for simulation model verification. It can provide more confidence in simulation models and increase the use of formal methods in the context of M&S by people that are not trained in formal techniques.