Article ID Journal Published Year Pages File Type
494148 Journal of Systems and Software 2007 15 Pages PDF
Abstract

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.

Related Topics
Physical Sciences and Engineering Computer Science Computer Networks and Communications
Authors
, ,