Automatic Selection of System Functional Scenarios for Formal Specification Animation

Functional scenario-based specification animation is a practical and effective technique for validating formal specifications but faces a scenario explosion problem. In this paper, we tackle this problem by proposing a new approach to selecting only consistent and meaningful functional scenarios in order to reduce the number of scenarios for animation. We define the concept of consistency for functional scenarios and describe how each of them can be automatically checked by means of a testing-based formal verification technique. We have applied the proposed technqiue to a railway card system to validate its applicability and present an example extracted from the application to illustrate how the proposed technqiues works in practice.