On Requirements Verification for Model Refinements

Conventional formal verification techniques rely on the assumption that a system's specification is completely available so that the analysis can say whether or not a set of properties will be satisfied. On the contrary, modern development lifecycles call for agile—incremental and iterative—approaches to tame the boosting complexity of modern software systems and reduce development risks. We focus here on requirements verification performed in the early exploratory stages on high-level models and we discuss how this can be integrated into an agile approach. We present a new technique to model-check incomplete high-level specifications against formally specified requirements. We do this in the context of incomplete hierarchical Statecharts, verified against a variation of CTL properties. Our approach supports step-wise specification and refinement verification. Verification can be incremental, that is alternative refinements may be separately explored and verification is only replayed for the modified parts. The results are presented by introducing the formalisms, the model-checking algorithm, and the tool we have implemented.