Yu Chen and Shaoying Liu, Hosei University, Japan

While formal specification is regarded as an effective means to capture accurate requirements and design, validation of the specifications remains a challenge. Specification animation has been proposed to tackle the challenge, but lacking an effective representation of the input/output data in the animation can considerably limit the understanding of the animation by clients. In this paper, we put forward a tool supported technique for visualization of the input/output data of processes in SOFL formal specifications. After discussing the motives of our work, we describe how data of each kind of data type available in the SOFL language can be visualized to facilitate the representation and understanding of input/output data. We also present a supporting tool for the technique and a case study to demonstrate the usability and effectiveness of our proposed technique. Finally, we conclude the paper and point out the future research directions.

Visualization, SOFL, Formal specification, Data type, Formal methods