An automated approach to specification animation for validation

Formal specification has been increasingly adopted for the development of software systems of the highest integrity. However, the readability of specifications for large-scale and complex systems can be so poor that even the developers may not easily understand whether their specifications define the “intended behaviors”. In this paper, we describe a software tool that supports the animation of specifications by simulating their functional scenarios using the Message Sequence Chart (MSC). The tool extracts automatically functional scenarios from a specification and generates a message sequence chart for each of them for a syntactic level analysis. The tool can also execute a functional scenario with test cases for a semantic level analysis if all the processes involved in the scenario are defined using explicit specifications. With the tool support the animation of a specification can be carried out incrementally to assist its user to review the adequacy of the specification. We present a case study applying the tool to animate a formal specification for a library system and evaluate its result.