Automatic analysis of consistency between implementations and requirements: a case study

Formal methods like model checking can be used to demonstrate that safety properties of event-based systems are enforced by the system´s requirements. Unfortunately, proving these properties provides no guarantee that they will be preserved in an implementation of the system. This paper describes a tool, called Analyzer, which discovers instances of inconsistency and incompleteness in implementations, and a case study of its use. Analyzer uses requirements information to check: that all state transitions implemented in the code are exactly those specified in the requirements. If programmers annotate their implementations with comments describing changes of values of requirements variables, our tool checks it against the requirements. Analyzer can also verify that the implementation is a model of user-specified safety properties. The tool can perform interprocedural analysis and verify properties which involve multiple state machines. In our case study, we analyzed the requirements and the implementation of a water-level monitoring system and discovered instances of inconsistency (testing incorrect conditions) and incompleteness (missing timing constraints) in the implementation