Integrating Animation-Based Inspection Into Formal Design Specification Construction for Reliable Software Systems

摘要

Software design has been well recognized as an important means to achieve high reliability, and formal specification can help enhance the quality of design. However, communications between the designer and the user can become difficult via formal specifications due to the potentially complex mathematical expressions in the specification. This difficulty may lead to the situation where the user may not be closely involved in the process of constructing the specification for quality assurance. To allow formal specification to play more effective roles in software design, we put forward a new approach to deal with this problem in this paper. The approach is characterized by integrating specification animation-based inspection into the process of constructing formal design specifications. We discuss the underlying principle of the approach by explaining how specification animation is utilized as a reading technique for inspection to validate, and then evolve, the current specification towards a satisfactory one. We describe a prototype software tool for the method, and present a case study to show how the method supported by the tool works in practice.