FeaVer: Model Extraction
The creation of a verification model that accurately captures the behavior of a systems implementation is typically the greatest obstacle that has to be overcome before automated verification techniques can be applied. Experts in model checking can spend weeks, and in some cases months, to gain sufficient familiarity with an application that they can manually construct and refine a model. Chances are that by the time such a model is completed and the verification process can start, it is out of date, or the project itself has progressed to a point where the verification results can only at great cost be used to revise the application.
The lookup tableThe FeaVer system uses a mechanical model extraction process that works with the help of a user constructed lookup table. The lookup table is used by the verifier to identify those aspects and portions of the implementation code that are deemed relevant to the verification task. Initially the user is likely to make some educated guesses about what is and what is not relevant. Inaccurate guesses do not have a negative impact on the verification process. The result of an inaccurate guess typically translates into a false failure report from the verifier, or failures to identify known existing behaviors that are used as markers in the model checking process.
With the help of the intial training runs with the model checker any gaps in the lookup table can be repaired. It usually does not take more than a few quick iterations of this type to obtain an accurate lookup table, causing the model checker to correctly identify the marker sequences and to reliably flag property violations.
MaintenanceThe lookup table is typically made once, at the start of a new verification project with FeaVer, and needs relatively minor effort to be kept up to date with changes that are made in the application, in the normal course of its design and maintenance.
The lookup table contains an entry for every unique statement and condition from the implementation code. To identify a statement as irrelevant to the verification task at hand, it is mapped to skip, the null-operation, in the model. To identify a condition as irrelevant it is mapped to both the boolean values true and false in the model, to indicate that the result of the evaluation of the condition is unspecified and could non-deterministically be either true or false.
Model templateEach data object that holds relevant information to the verification task (such as the data field that records the on- and off-hook state of a subscriber line in a call processing application) is represented in abstract form in the verification model. All manipulations and tests of the values of that object are then also mapped to the corresponding manipulation or test of the abstract object in the verification model. To complete the definition of the lookup table, therefore, the user also adds a small number of variable definitions into a predefined template for the verification model. Unless the number of variables that needs to be tracked by the model checker changes, the template definitions are only entered once at the start of the project, and need little or no maintenance thereafter.
Test driversThere is one more part of the model template that the user has to define: a definition of the environment in which the implementation is assumed to execute. For a call processing application this environment consists of local subscribers connected to the switch, and remote switches that can initiate and respond to commands from the local switch. This environment definition can be thought of as a set of simple test drivers that one would built for a more traditional testing application.
|Back to Main Page|