A contract-based method to specify stimulus-response requirements
This work addresses the gap between formal requirements and executable code for engineers, but it is incremental as it builds on existing formal methods.
The authors tackled the problem of translating declarative stimulus-response requirements into imperative programs by introducing a method for specification and verification using program routines with conditionals and assertions, and applied it to the Landing Gear System ASM model.
A number of formal methods exist for capturing stimulus-response requirements in a declarative form. Someone yet needs to translate the resulting declarative statements into imperative programs. The present article describes a method for specification and verification of stimulus-response requirements in the form of imperative program routines with conditionals and assertions. A program prover then checks a candidate program directly against the stated requirements. The article illustrates the approach by applying it to an ASM model of the Landing Gear System, a widely used realistic example proposed for evaluating specification and verification techniques.