Automated Visualization of Input/Outpue for Processes in SOFL Formal Specifications

摘要

While formal specification is regarded as an effective means to capture accurate requirementsand design, validation of the specifications remains a challenge. Specification animation hasbeen proposed to tackle the challenge, but lacking an effective representation of the input/outputdata in the animation can considerably limit the understanding of the animation by clients. Inthis paper, we put forward a tool supported technique for visualization of the input/output dataof processes in SOFL formal specifications. After discussing the motives of our work, wedescribe how data of each kind of data type available in the SOFL language can be visualized tofacilitate the representation and understanding of input/output data. We also present asupporting tool for the technique and a case study to demonstrate the usability and effectivenessof our proposed technique. Finally, we conclude the paper and point out the future researchdirections.