There has been considerable interest in verifying safety properties of tabular form requirement specifications of event-driven systems. This has led to development of automatic model checkers i.e. tools that verify whether an automaton representing the system is a model of formulas expressing safety properties of the specifications. However, we do not have any automated methods to verify the adequacy of an implementation with respect to requirements.
We describe Analyzer - a tool that takes a set of requirements in the form of a mode transition table, and annotated C code that implements them, and checks whether the requirements are implemented correctly. From the annotations and the control flow structure of the C program, Analyzer checks for consistency (i.e. whenever the mode in the implementation changes, there is a valid transition from the previous to the new mode in the requirements), and completeness (i.e. every transition specified in the requirements is implemented). Analyzer uses data-flow analysis to generate a set of all possible modes at a given point of the program. The language for annotating the code consists of statements describing values of system variables and global modes representing sets of system states. The annotation language is small and easy to use as it only requires the programmer to have knowledge of a local behavior of the program.
We used Analyzer to test several implementations of a Temperature Control System - a simple event-driven system, and found that it is capable of detecting both errors of commission and omission. We are currently conducting a larger case study. One of the drawbacks of our present system is that each function has to be verified every time it is called. However, it only takes seconds to verify a relatively complex program. Analyzer does not verify the code itself, and annotations can be introduced at any level of granularity; therefore, we believe that Analyzer is useful for verifying implementation of both detailed and high level specifications.