A Method for Improving the Verification and Validation of Systems by the Combined Use of Simulation and Formal Methods

Verification and Validation (V&V) of Systems is an important process in the development of systems, in order to ensure that they are reliable and operational. Among methods of V&V, there are two that seem to be opposite to each other: simulation, which is empirical, and formal verification, which is comprehensive. Moreover, simulation and formal verification propose many different formalisms, increasing the gap between them. But, jointly used, these two powerful tools allow making a more efficient verification, increasing the confidence we can put in the verified systems. The main problem is how we can combine their use and how we can reduce the gap created by the nature of both of them. This paper presents guidelines and a general approach in order to use simulation, and especially discrete-event simulation, on a model specified in a verifiable formal language.