A simulation approach to verification and validation of formal specifications

Specification simulation is an approach to verifying and validating specifications by well-selected sample data. In this paper we put forward a technique for simulation of formal specifications in order to detect potential faults and validate their desired functions. The important benefit of this technique is it allows us to simulate implicit specifications, which are usually defined with a pair of pre- and postconditions and may not be executable. We discuss ways of simulation case generation, evaluation of logical expressions, and simulation result analysis, and demonstrate how they are applied in practice by examples.