Sofl specification animation with tool support

Abstract

Formal specification animation is a very useful technique for verification and validation. It provides the end users and field experts with an intuitive way to observe the operational behaviour of software system described by the formal specification. Several tools have already been built to support animations of specifications written in different formal languages. In this paper, we describe the design of a tool that can support the animation of specification written in Structure Object-oriented Formal Language (SOFL). The animation strategy underlying the tool uses system functional scenario as a unit and data as connection among independent operations involved in one system functional scenario. A system functional scenario defines a behaviour that transforms input data into the output data through a sequential execution of operations. It is the target of animation. In the animation, data is used to connect each operation in a specific scenario. The data can be provided by the user or generated automatically. It will help the user and the developer to understand the system. We explain the whole animation process step by step and present a prototype at the end of the paper. © 2014 Springer International Publishing Switzerland.