Refactoring design models for compositional verification, conformance testing, and inductive verification

Although automated finite-state verification techniques have matured considerably in the past several years, they are invariably applicable only to simplified, idealized models of systems. Finding the right design abstractions and organizing a model to be amenable to automated verification, avoiding the well-known state explosion problem, is a creative task that cannot be fully automated. Nonetheless, some formal relation between the verified model and the "as-built" structure of the software system is required to gain confidence in their consistency, e.g., through conformance testing. One way to maintain the relation is by constructing one of the structures by transforming the other.; We describe how as-built design models can be refactored for compositional state-space analysis. The process is semi-automated (the designer must choose from among a set of idiomatic transformations, but each transformation is applied and the behavioral equivalence is checked automatically). We show how such refactoring transformations are used to obtain models that can be hierarchically composed, avoiding excessive state explosion. Since the refactoring transformations are checked, the original model of the system structure "as-built" can be used to generate conformance test oracles relating the actual system to the refactored, verified design. We argue that this indirect, two-phase approach is more sensitive than direct specification-based testing of implementations.; Our refactoring can also be applied to systems parameterized by infinite control parts, such as systems composed of many identical processes. These systems can sometimes be verified inductively using a network invariant, but systems whose component processes vary in some systematic way are not amenable to direct application of that method. We describe how variations in behavior can be "factored out" into additional processes by refactoring, thus enabling induction over the number of processes.