Automated Functional Scenarios-Based Formal Specification Animation

The validation of formal specifications before their implementation can help to detect errors of systems in early stages of development and reduce the entire cost significantly. Formal specification animation is developed as an effective technique for this purpose. Animation gives the end users and field experts an intuitive way to observe the operational behavior of specification without being distracted by its complex syntax. Several tools have already been built to support specification animation. But most of these tools need a translation from a formal specification language to an executable programming language. In this paper, we propose a novel animation approach called Automatic Functional Scenarios-based Animation. This approach uses data as connection among independent operations involved in a specific behavior to "execute" specifications, and does not translate them to program. We explain how to generate necessary data for animation by modifying an automatic operation function scenario-based test case generation method, and present a case study of applying this animation approach to SOFL specification.