|
Draft
Model-Based Verification (MBV) is a systematic approach for
detecting defects (errors) in software requirements, designs, or code
[Gluch
98]. The approach incorporates the use of mathematical models
to provide a disciplined and logical analysis practice rather than a
"proof" of correctness strategy. MBV involves creating essential
models of system behavior and analyzing these models against formal
representations of expected properties.
Essential models are simplified formal representations that
capture the essence of a system rather than providing an exhaustive,
detailed description of it. By selecting a system's critical
(important or risky) parts and appropriately abstracted perspectives,
a reviewer using model-based techniques can focus the analysis on the
critical and technically difficult aspects of the system. Driven by
the discipline and rigor required in the creation of a formal model,
simply building the model uncovers errors.
Once the formal model is built, it can be checked using automated
model checking tools. This analysis reveals potential defects while
formulating claims about the system's expected behavior. Model
checking has been shown to uncover even the most difficult to
identify errors&emdash;those that result from the complexity
associated with multiple interacting and interdependent components.
These include embedded and highly distributed applications.
MBV consists of a set of engineering practices for identifying and
guiding the correction of defects in software artifacts. These
practices are founded upon formal modeling and analysis techniques.
As shown in Figure 1, MBV practices can be divided into two distinct
categories of activities:
1. Project level (team) activities
2. Engineering (individual) activities
Figure 1. Model-Based Engineering Activities
Project level activities involve both programmatic and technical
decisions and engage multiple members of the project team in
important decisions. These decisions relate to defining the
scope (how much of the system is to be modeled and analyzed),
formalism (what techniques are to be employed), and
perspective (what aspects of the system are to be considered)
involved in the effort.
The bulk of the engineering activities in MBV are principally
individual. Each engineer builds and analyzes models and compiles
defects independently. While building MBV models, the systematic
framework, attention to detail, and discipline demanded by the
modeling techniques can lead to the identification of defects. During
the analysis activities, automated model checking techniques are used
to investigate the system's complexities and behavior and to identify
elusive logic errors. While the individual engineer has principal
responsibility for MBV activities, it is often valuable to
collaborate with other experts. This is especially true during the
analysis phase where additional domain expertise can help to focus
the effort. Throughout the process, engineers compile the identified
defects and the results of their analyses.
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 overhead costs 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 higher quality software at a lower cost.
MBV will allow a practitioner to:
- Detect errors early. Since it can be used for
requirements and preliminary design analysis of a system
development, MBV offers the potential to detect errors early in
the design process before they propagate into the design or
code.
- Detect 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 handle complexity. MBV technology addresses
system complexity that is difficult for humans to verify even
through extensive individual review of the problem.
- Identify 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) These editing-like activities can be effectively and
efficiently accomplished through MBV automated checking.
- Develop partial and targeted analyses. The MBV approach
can be applied to all or part of the system. This enables its
efficient use in complex systems where the analysis can be
targeted to only the critical areas of system.
- Apply 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.
A number of published studies have cited successful implementation
of the MBV approach for model checking for digital hardware and
complex protocol systems. Some examples include:
- IEEE standard Futurebus+ cache coherence
protocol&emdash;Although development began four years earlier
and validation efforts had been conducted, model checking
identified a number of previously undetected errors [Clarke
95].
- High Speed Communications IC Chip&emdash;During field
tests of a complex high-speed communications IC chip, errors in
the form of duplicated and lost data were observed. Model checking
was able to help identify the cause of this error very quickly.
Using simulation or other conventional techniques would have been
impractical because it would have required an extraordinarily
amount of time and resources [Fujita
96].
- Power PC &emdash; Model checking was employed to
diagnose the cause of a design error found during hardware testing
of the PowerPC 620 microprocessor. This error eluded detection
despite extensive simulation and standard verification. Model
checking techniques could have detected the error early in the
design phase [Raimi
97].
The specific techniques and engineering practices of applying MBV
to software verification have yet to be fully explored and
documented. A number of barriers to MBV adoption have been identified
including the lack of tool support, expertise in organizations, good
training materials, and process support for formal modeling and
analysis.
In order to address some of these issues, the Software Engineering
Institute (SEI) has created a process framework for MBV practice.
This process framework identifies a number of key tasks and
artifacts. Additionally, the SEI is working on a series of technical
notes that can be used by MBV practitioners. Each technical note is
focused on a particular MBV task, providing guidelines and techniques
for one aspect of the MBV practice. Currently, the technical notes
that are planned address abstraction in building models, generating
expected properties, generating formal claims, and interpreting the
results of analysis.
There are some limitations and barriers that determine how and
when MBV can be effectively applied:
- Domains: Although MBV can in theory be applied to any
software system, the technique is more productive in systems that
involve real-time constraints, concurrency, distribution, or
complex interactions among components.
- Process maturity: In order to be effective, MBV
requires product artifacts that can easily be converted into
models. For example, if MBV is being applied to a requirements
specification, the requirements should be stated with a level of
detail and rigor sufficient to create meaningful, reasonably
complex models. In general, MBV will work better in mature
organizations that produce sufficiently detailed and rigorous
documents.
- Training and expertise: Although MBV does not require
the mathematical background necessary to apply heavy formal
methods, it does require some basic knowledge of formalisms and
formal notations. This will hold true until more commercial tools
simplify and automate MBV practices. Even more important than
formal methods training is a practitioner's knowledge of the
system under consideration.
Traditional formal methods are an alternative to MBV for critical
systems. However, they are generally more expensive and require more
expertise than MBV. On the other hand, traditional formal methods can
be used to help prove the correctness of software whereas MBV can
only increase the confidence in the system correctness.
MBV can be included as part of a peer review team process
[Software
Inspections]. The specific activities of the MBV reviewer(s)
are coordinated with those of the traditional review team. As part of
a review team, an individual MBV reviewer's principal responsibility
is much the same as an individual reviewer in a conventional
inspection&emdash;identify defects in the artifact under review
[Gluch
99].
MBV can potentially be applied in the context of Cleanroom
Software Engineering. The focus of Cleanroom involves moving from
traditional, craft-based software development practices to rigorous,
engineering-based practices. Cleanroom software engineering yields
software that is correct by mathematically sound design, and software
that is certified by statistically-valid testing. Reduced cycle times
result from an incremental development strategy and the avoidance of
rework.
This technology is classified under the following categories.
Select a category for a list of related topics.
|
[Clarke 86]
|
Clarke, E.; Emerson, E.A.; & Sistla, A.P. "Automatic
Verification of Finite State Concurrent Systems Using
Temporal Logic Specifications," ACM Transcripts on
Program Language Systems 8, 2 (1986): 244-263.
|
|
[Clarke 95]
|
Clarke, Edmund M., et al. "Verification of the Futurebus+
Cache Coherence Protocol." Formal Methods in System
Design 6, 2 (March 1995): 217-232.
|
|
[Fujita 96]
|
Fujita, M. "Debugging a Communications Chip." IEEE
Spectrum 33, 6 (June 1996): 64.
|
|
[Gluch 98]
|
Gluch, D. & Weinstock, C. Model-Based
Verification: A Technology for Dependable System Upgrade
(CMU/SEI-98-TR-009, ADA 354756). Pittsburgh, Pa.: Software
Engineering Institute, Carnegie Mellon University, 1998.
Available WWW: <http://www.sei.cmu.edu/publications/documents/
98.reports/98tr009/98tr009abstract.html>
|
|
[Gluch 99]
|
Gluch, D. & Brockway, J. An Introduction to
Software Engineering Practices Using Model-Based
Verification (CMU/SEI-99-TR-005, ESC-TR-99-005).
Pittsburgh, Pa.: Software Engineering Institute, Carnegie
Mellon University, 1999. Available WWW: <http://www.sei.cmu.edu/publications/documents/
99.reports/99tr005/99tr005abstract.html>
|
|
[Harel 87]
|
Harel, D. "Statecharts: A Visual Formalism for Complex
Systems." Science of Computer Programming 8, 3 (June
1987): 231-274.
|
|
[Holt 99]
|
Holt, A. "Formal Verification With Natural Language
Specifications: Guidelines, Experiments And Lessons So Far."
South African Computer Journal 24 (November 1999):
253-257.
|
|
[McMillan 92]
|
McMillan, K.L. Symbolic Model Checking: An Approach to
the State Explosion Problem (CMU-CS-92-131). Pittsburgh,
Pa.: Computer Science Department, Carnegie Mellon
University, 1992.
|
|
[Raimi 97]
|
Raimi, R. & Lear, J. "Analyzing a PowerPCTM 620
Microprocessor Silicon Failure Using Model Checking,"
964-973. Proceedings of the International Test Conference
1997, Washington, D.C., November 1-6, 1997.
|
Chuck Weinstock, Software Engineering Institute
20 Mar 2001: Original
The Software
Engineering Institute (SEI) is a federally funded research and
development center sponsored by the U.S. Department of Defense
and operated by Carnegie Mellon University.
Copyright
2007
by Carnegie Mellon University
Terms of Use
URL: http://www.sei.cmu.edu/str/descriptions/mbv_body.html
Last Modified: 11 January 2007
|
