Tool Support for Rigorous Formal Specification Inspection

A dependable system must be internally consistent. In order to implement a dependable system, any inconsistency in the design of the system must be eliminated before it can be implemented. In this paper, we describe a tool supported inspection method that can help inspectors effectively and efficiently exam the system specification for detecting inconsistency. The underlying inspection principle is called Rigorous Inspection Method (RIM). This inspection principle uses functional scenarios and consistency properties as guidelines for carrying out inspection. The functional scenarios present the system behaviours which show the inspector what need to be inspected. And the consistency properties serve as a checklist and tell the inspector what aspects of the system need to be examined. We designed the specific methods of deriving functional scenarios and generating inspection tasks by applying consistency properties to each scenario. We implemented these specific methods in a support tool and present the prototype at the end of this paper.