A formal specification animation method for operation validation

Formal specification can benefit software quality by precisely defining the behaviors of operations to prevent primary mistakes in the early phase of software projects, but a remaining challenge is how such a specification can be checked comprehensibly to show whether it satisfies the user's perception of requirements. In this paper, we describe a new technique for animating operation specifications as a means to address this problem. The technique offers new ways to do (1) automatic animation data generation for both input and output of an operation based on pre- and post-conditions, (2) visualized demonstration of the relationships between input and the corresponding output, (3) comprehensible animation of data items, and (4) illustrative animation of logical expressions and the operators used in them. We discuss these issues and present a prototype tool that supports the automation of the proposed technique. We also report an industrial application as a trial experiment to validate the technique. Finally, we conclude the paper and point out future research directions.