NEWS AT SEI
This article was originally published in News at SEI on: March 1, 2001
Formal methods have long offered the promise of ensuring high quality software using mathematical rigor. Note that this issue's director’s message points to one article suggesting that 40 to 50 percent of programs contain nontrivial defects. Formal methods represent a clear attempt to address such concerns. However, applying traditional formal methods to a complete system design requires a significant investment–from learning a difficult technology to applying it in all phases of the development effort. As a result, there have been relatively few success stories, and formal methods have failed to achieve widespread adoption.
The SEI has leveraged the work of the formal methods community to develop a software engineering practice known as model-based verification (MBV). MBV involves the selective use of formal methods on abstract models of important portions of a system, thereby providing many of the benefits promised by formal methods without the associated high cost.
Model-based verification makes use of "light weight" formal methods and can be used throughout the software life cycle. For example, MBV can be used to augment the standard peer review process to find subtle errors that would not typically be found in such a process. The term "light weight" is used to underscore the fact that MBV relies on selective, focused use of formalism as well as mathematically based techniques not generally classified as formal methods.
MBV makes use of existing techniques such as model checking, in which abstract models of a system are built to capture the salient features of the system or a portion of the system that is considered important. For example, a traffic signal system at an intersection could be modeled at any number of levels: "You may want to model each of the four lights as it goes from green to yellow to red and how they interact with each other," says Chuck Weinstock of the SEI. "Or you may only care that the lights align so that the traffic going one way is stopped when the traffic going perpendicular is moving. Or you may only care that a single light works." MBV allows you to select the abstraction level and then apply the appropriate methods to it.
Once the model is built, it is tested against claims, also written in a formal language. In the traffic signal example, these claims might be the following: "conflicting directions will never be green at the same time," or "at least one direction will always be green." A tool known as a model verifier would then be used to determine whether the claims are satisfied. "If the model has been correctly built," says Weinstock, "when a negative result comes back, you should be able to go back to the code and find the error."
Benefits of MBV
A key benefit of MBV is that it allows software engineers to find subtle errors and to find them earlier in the life cycle when they are cheaper to fix. "We believe that if MBV reveals even one very subtle error that was not found otherwise," says Weinstock, "it will more than pay for itself." The models also serve as system documentation that otherwise would not exist. Because the model is precise at the abstract level, the documentation can provide a great deal of precision about how the system is supposed to behave. A better understanding of the system allows for easier life cycle support.
In addition, MBV is built on established techniques. Model checking is used routinely in complex hardware design and has been used successfully in protocol design. For example, when one organization wanted to test its new model checking tool, it tested the tool on a new product that it considered complete and ready for release. The product was seeded with a few errors and the tool was applied to see whether the tool would find the errors. The tool found not only the errors that were seeded, but additional errors that would have required the system to be recalled if it had been released.
As noted above, formal methods can be expensive to apply. "Furthermore," says Weinstock, "it typically takes people with highly specialized knowledge to use formal methods. By contrast, the basics of MBV can be learned by a good software engineer in a week or so of training and study."
Putting MBV into Practice
SEI staff are currently codifying MBV into a software engineering practice and transitioning the practice to the software community through the use of courses, handbooks, and pilot studies. A half-day version of an MBV tutorial was given at the SEI Software Engineering Symposium in September 2000. A full-day version is being developed and a draft MBV handbook is in progress.
A pilot study is currently being conducted with NASA, and involves the X33 Reusable Launch Vehicle. The information gathered will help to refine MBV, making it more suitable for broad adoption in the software engineering community.