USING ABSTRACTION AND MODEL CHECKING TO DETECT SAFETY VIOLATIONS IN REQUIREMENTS SPECIFICATIONS

Exposing inconsistencies can uncover many defects in software specific ations. One approach to exposing inconsistencies analyzes two redundan t specifications, one operational and the other property-based, and re ports discrepancies. This paper describes a ''practical'' formal metho d, based on this approach and the SCR (Software Cost Reduction) tabula r notation, that can expose inconsistencies in software requirements s pecifications. Because users of the method do not need advanced mathem atical training or theorem proving skills, most software developers sh ould be able to apply the method without extraordinary effort. This pa per also describes an application of the method which exposed a safety violation in the contractor-produced software requirements specificat ion of a sizable, safety-critical control system. Because the enormous state space of specifications of practical software usually renders d irect analysis impractical, a common approach is to apply abstraction to the specification. To reduce the state space of the control system specification, two ''pushbutton'' abstraction methods were applied, on e which automatically removes irrelevant variables and a second which replaces the large, possibly infinite, type sets of certain variables with smaller type sets. Analyzing the reduced specification with the m odel checker Spin uncovered a possible safety violation. Simulation de monstrated that the safety violation was not spurious but an actual de fect in the original specification.