This paper presents an analysis tool, Analyzer, to verify that a system's requirements are preserved in its concurrent implementation. Analyzer uses SCR-expressed requirements information to automatically generate properties which ensure that required state transitions appear in the model of implementation. In addition, Analyzer verifies that the implementation satisfies user-specified safety properties.
There has been active interest in verifying properties of concurrent systems. Most of the suggested approaches analyze rendezvous-based communications without considering the data-flow. If programmers annotate their implementations with comments describing changes of value of requirements variables and communication patterns, our analysis tool can verify properties involving both data-flow and communication information.
The tool uses the annotations and the control-flow information to compute reaching values of requirements variables at every state of each process. A model-checking algorithm checks if automatically-generated properties hold in every state. It also takes possible compositions of process states and checks if user-specified properties hold.
To validate this technique, we conducted a case study where we analyzed the requirements and the implementation and proved a variety of properties of a Nuclear Control Rod system.