Animation is a technique to dynamically present the behaviors of formal speci…cations. It gives the user and expert a chance to observe the operational behaviors of the speci…cation and enhance their con…dence before the speci…cation is implemented. After extensively studying of the literature, we …nd that several techniques have been developed for animating or dynamically presenting formal speci…cations, however, no work has explored the same approach as we propose in this dissertation to utilize speci…cation animation as a reading technique to assist speci…cation inspection.
As far as speci…cation animation is concerned, most of the existing work we have discovered take the approach that …rst transforms the formal speci…cation into executable code written in a programming language and then animate the speci…cation by executing the code. PiZA [101] is an animator for Z formal speci…cation. It translates Z speci…cations into Prolog to generate outputs. Similarly, an animation approach for Object-Z speci…cation is described in [102], which translates the Z speci…cation into C++ code for execution. Morrey et al. developed a tool called “wiZe” to support the construction of model-based speci…cation language, in particular Z, and the animation of an executable subset of Z speci…cation language [103]. The subtool for animation of speci…cations is called ZAL. The wiZe is responsible for making a syntactically correct speci…cation and transforming it into
an executable representation in an extended LISP, and then passes the executable representation to ZAL. ZAL animates the speci…cation by executing the speci…cation with test cases.
PVS (Prototype Veri…cation System) [45] is a speci…cation and veri…cation system including an expressive speci…cation language and interactive theorem prover. It includes a ground evaluator [104] that can translate an executable subset of PVS to Common Lisp and provides a read-eval-print loop for testing the translated Lisp program. In [105], the PVS is enhanced from two points for evaluation and animation purposes. One enhancement is the extension of the ability of executing PVS speci…cation. A technique called “semantic attachment”is introduced.
It allows the user to provide their own executable program segments to di¤erent PVS functions, therefore some PVS speci…cation that cannot be translated by the ground evaluator can be executed. And another enhancement is to animate the PVS speci…cation by displaying the results of ground evaluator in the Graphical User Interfaces (GUIs) created by Tcl/Tk.
In [68], Liu and Wang introduced an animation tool called SOFL Animator for SOFL speci…cation animation.
It can be used to perform syntactic and semantic analysis of a speci…cation. When performing an animation, the tool will automatically translate the executable subset of SOFL speci…cation into Java program segments, and then use some test case to execute the program. In order to provide a graphic presentation of the operational behaviors of speci…cation, SOFL Animator uses Message Sequence Chart (MSC) to present the execution of the translated Java program.
MSC is also adopted in other animation approach as a framework to provide a graphical user interface to represent animation. Stepien and Logrippo built a toolset to translate LOTOS traces to MSC and provide a graphic animator [106]. The translation is based on the mappings between the elements of LOTOS and MSC.
Combes and his colleagues described an open animation tool for telecommunication systems in [107]. The tool is named as ANGOR, and it o¤ers an environment based on a ‡exible architecture. It allows animating di¤erent animation sources, such as formal and executable language like SDL and scenario languages like MSC.
VDMTools is an industry-strength toolset supporting the analysis of system models expressed in VDM [70] and has been successfully used in several industrial projects [108] [109] [110]. The interpreter inside the VDMTools can execute a large executable subset of VDM speci…cation. User can test the VDM speci…cation by providing test cases and observe the system behavior by setting breakpoints or stepping. Moreover, the interpreter in VDMTools
can automatically create an external log…le recording all the events happened during an execution. In this log…le, each event is tagged by the time at which it occurs, this information can be used to graphically display all the events on a time-axis. Overture [111] provides functions similar to VDMTools and is built on an open and extensible platform based on the Eclipse framework. By using the combinatorial testing function [112], a large collection of test cases can be executed to detect the run-time errors caused by forgotten pre-condition or violation of invariant and post-condition.
ProB [69] [113] is a validation toolset for B-Method. It can automatically check the consistency of B speci…cation via model checking. The model checker in ProB explores the state space of a speci…cation and determine whether a state violate an invariant. It can graphically display the path from an initial state to a counter-examples when a violation of invariant is discovered. However, in order to perform the exhaustive model checking, the given sets must be …nite, and the integer variables must be restricted to a small range. The animation of B speci…cation is carried out by separating the model checking process. Start from the initial state, in each step of the animation, the user can choose an action to proceed to the next state.
Another tool that adopts model checking for presenting the dynamic behavior of systems is UPPAAL [72] [114], which allows user to model the system behavior in terms of states and transitions between states. Unlike Z, B, or VDM, there is no article speci…cation in UPPAAL. User can set invariants to each state, and set guards and action to each transition. The invariants describe the condition that should be satis…ed by the state; the guards restrict the possible state changes by disabling transitions; and the actions change the value of variables. To animate the model, thesimulator of UPPAAL can explore the state space of the model in a step-by-step fashion.
Time Miller and Paul Strooper introduced a framework for animating model-based speci…cations by using testgraphs [67]. The framework provides a testgraph editor for users to edit testgraphs, and then derive sequences for animation by traversing the testgraph. Gargantini and Riccobene proposed an automatically driven approach to animating formal speci…cations in Parnas’ SCR tabular notation [115]. One important feature of this work is the adoption of a model checker to help …nd counter-examples that contain a state not satisfying the property to be established by animation. The advantage of this work is that the formal speci…cation can be checked by means of model checking in the animation.
Some of the existing studies, like PVS ground evaluator, wiZe, and SOFL Animator, require an automatic
translation of the formal speci…cation into an executable programming language. This will inevitably limit the capability of animation because speci…cations using pre- and post-conditions may not be automatically transformed into code in general. Therefore, what these animation tools can do is only to deal with a subset of the formal notations mentioned above. In contrast to this situation, our animation approach described in this dissertation does not require any translation of the speci…cation into code; it can directly perform animation by evaluating the pre-and post-conditions of the processes involved in the target system scenarios for the selected test cases pre-and expected results. This is much easier to implement technically and capable of dealing with all pre-post style speci…cations.
VDMTools and Overture also evaluate the pre- and post-conditions but in the run-time of executing test cases.
However, only a large subset of VDM speci…cation can be executed and explicit speci…cation must be constructed for execution. The explicit speci…cation is an algorithm solution of an operation in VDM. The speci…cation contains only pre- and post-conditions cannot be executed. The animation tools based on model checking, like ProB and UPPAAL, have inherent challenge of state explosion, the states of the system must be …nite. Although our animation approach has similarities with some exiting studies, no exiting work adopts animation as a reading technique to guide the user read through the speci…cation for inspection purpose.