Model-Based Verification
Essential Models
Formal Models
Modeling
Model Checking
Successes
Potential Benefits
Work With Us
Model-based verification (MBV) combines established software modeling techniques, including formal methods, with innovative model checking approaches. MBV integrates these techniques into proven software engineering review and testing processes. This integration defines a systematic practice for finding and correcting errors in software requirements, design specifications, and code.
Essential Models
MBV relies on the creation and analysis of "essential" models of a system. Essential models are abstract representations that establish multiple perspectives on a system. These perspectives involve two categories of models:
- focused representations (partial models): abstract representations of critical, high risk parts of the system
- generalized abstractions: broad, single perspective views of the entire system (e.g., representing only the transitions that occur in a system)
return to top
Formal Models
There are a variety of approaches that comprise the MBV suite of techniques. These are newly emerging in academic and corporate research communities as well as some that are being used in commercial hardware development (e.g., microprocessor design). Most approaches involve the use of formal methods but because of their use in the form of simpler essential models, rather than as detailed specification methods, they are referred to as the lightweight use of formal methods.
return to top
Modeling
The action of modeling (systematic translation into a "formalized" representation) itself provides substantial insight into system capabilities, limitations, and errors. Regardless of the artifact under review the result is a precise and consistent description, which can become part of the collection of artifacts that support development or upgrade engineering processes.
return to top
Model Checking
Model checking is a form of model-based verification where an automated tool is used to check a model of a system against its expected properties. The output of the checking tool is either a confirmation that each property is maintained or a non-confirmation, in which case a counter example is provided. For example, a model of a missile launch system is checked against the expected property that the missile will not be launched (engines ignited) unless all the release latches are disengaged. If this is the case the model will confirm its validity. If it is not true it will show what states or portions of the model (a counter example) will result in the premature launch. Figure 1 depicts the model checking process.
Figure 1. Model Checking
return to top
Successes
The use of a model-based verification approach in the form of model checking for digital hardware and complex protocol systems has been successful in a number of published studies. Some examples include analyses of:
IEEE standard cache coherence protocol of the Scalable Coherent Interface
— Created a model from the C code and found several errors including omitted variable initializations and subtle logic errors. These errors were found even though the protocol had been extensively discussed, simulated, and implemented.
IEEE standard Futurebus+ cache coherence protocol
— Although development began four years earlier and informal validation efforts had been conducted, the analysis identified a number of previously undetected errors.
HDLC transmitter (an application specific hardware library component) at Bell Labs
— Because of the maturity of the design (essentially complete) no errors were expected. However, a critical error was found that would have reduced the throughput of the HDLC channel and possibly resulted in lost transmissions.
ISDN protocol at AT&T
— Formal modeling and automated verification techniques were used to efficiently identify and fix a number of errors.
return to top
Potential Benefits
MBV is a pragmatic application of formal methods that focuses on error (defect) identification rather than formalized specification or proofs. This approach capitalizes on the advantages provided by formal methodologies without incurring the costly overhead normally associated with them.
It is expected that the MBV technology and practices will increase the effectiveness of verification and test activities and will result in lower cost and higher quality software upgrades.
Potential benefits include:
detecting subtle errors — Especially promising is the potential for the early detection of subtle and potentially costly errors (defects) that are not identified even in extensive testing. Often these errors are not recognized until the software is in the field.
effectively handling complexity — MBV technology addresses system complexity that is difficult for humans to verify even through extensive individual review of the problem.
detecting errors early — Since it can be used for requirements and preliminary design analysis of a system upgrade or new system development, MBV offers the potential to detect more errors early in the design process before they propagate into the design or code.
identifying basic errors — The large size and complexity of software systems complicates verification by significantly increasing the amount of mundane checking that is needed (e.g., that there is consistent naming and use, that all the terms are defined, etc.) These editing-like activities can be effectively and efficiently accomplished through MBV automated checking.
flexibility for partial and targeted analysis — The MBV approach can be applied to all or part of the system. This enables its efficient use in upgrades of complex systems where the analysis can be targeted to only the upgraded parts of the system or to critical areas of system.
usefully applied in all phases of development — The modeling checking technique that is part of the MBV approach has been used for error detection in requirements, design, and code. It can be used as the foundation for testing by helping to define test strategies, test cases, and critical areas that require focused or more extensive testing.
return to top
Work With Us
The SEI is seeking collaboration partners to investigate the effectiveness
of MBV in solving real-world problems. For more information contact
SEI Customer Relations
Phone: 412 / 268-5800
FAX: 412 / 268-5758
E-mail: customer-relations@sei.cmu.edu
or access the Performance Critical Systems Web
site
return to top
|
MBV Related Tools
|
VTU main page
Dynamic Systems
|
Performance Critical Systems