Reviewing Formal Specification for Validation Using Animation and Trace Links

Formal specification has proved to be an effective technique for precisely defining software functionality, but validating it against the user\´s requirements still remains a challenge. In this paper, we propose a novel and practical review approach that utilizes specification animation and trace links to support the reviewing of formal specifications for their validation. The scenario-based animation method dynamically presents the specification to the reviewer by means of "executing" it in a step-by-step manner. It is adopted as a reading technique to guide the reviewer to read the specification and provides him with clear review targets. The trace links that connect the specification to the user\´s original requirements supply the reviewer with necessary information for determining whether defects are found. We first explain the scenario-based animation and trace links respectively and then propose a group of criteria for validating the formal specification. A case study is described to illustrate the review process at the end of the paper.