Validating formal specifications using testing-based specification animation
Shaoying Liu · 2016
Software requirements analysis and design can significantly benefit from writing formal specifications in some circumstances but meanwhile face challenges in validating the specifications. In this paper, we propose a specification animation technique to deal with the challenging issues. The technique is characterized by utilizing test case generation from formal operation specifications to carry out visualized demonstration of the input-output relation of the operation. With the animation technique, the analyst and the client can be facilitated to check the desirability of the specification. We describe a set of test case generation criteria based on both the specification structure and the client's requirements, and discuss how visualized demonstration can be implemented. We also present a small experiment to evaluate the effectiveness of our technique and briefly explain the potential challenges for future research.