A Rigorous Method for Inspection of Model-Based Formal Specifications

Writing formal specifications can help developers understand users´ requirements, and build a solid foundation for implementation. But like other activities in software development, it is error-prone, especially for large-scale systems. In practice, effective detection of specification errors still remains a challenge. In this paper, we put forward a rigorous, systematic method for the inspection of model-based formal specifications. The method makes good use of the well-defined consistency properties of a specification to provide precise rules and guidelines for inspection. The inspection process utilizes both well-defined expressions derived from the specification and human inspectors´ judgments to find errors. We present a case study of the method by describing how it is applied to inspect an Automated Teller Machine (ATM) software specification to investigate the method´s feasibility, and explore potential challenges in using it. We also describe a prototype software tool including its functions and distinct features to demonstrate the tool supportability of the method.