The current focus in logic model checking in
software verification targets the
elimination of the need for hand-constructed models.
In the
FeaVer project we used automated model extraction
from C code to address this problem.
In this talk I will describe a new, and possibly simpler, method, that allows us to
link a logic model checker (e.g., Spin)
directly to unmodified application level code.
We now write a non-deterministic test-harness as a Spin model,
to drive the application through all its relevant states, while
the model checker verifies its logic properties.
Notably, the model checker can use powerful data abstraction techniques
in this verification process,
while the application uses only concrete data representations.
I'll give some examples of the application of this method to
the verification of critical pieces of flight software for a
recent JPL mission.
About the speaker:
Dr. Gerard J. Holzmann is perhaps best known as the designer of the Spin model checker, which was recognized in 2001 with the ACM Software Systems Award. Formerly a Director of the Computing Principles Research group at Bell Labs in Murray Hill, NJ, Holzmann joined NASA's Jet Propulsion Laboratory in 2003 to start a new Laboratory for Reliable Software. Holzmann holds 7 patents, one of which received the 2003 Thomas Alva Edison Award in Information Technology from the Research and Development Council of New Jersey. He has written several books, including "The Spin Model Checker" (Addison-Wesley, 2004), "The Early History of Data Networks" (IEEE CS Press, 1995), and "Beyond Photography: The Digital Darkroom" (Prentice Hall, 1987).
Other Links of Interest:
Gerard Holzmann's Homepage Gerard Holzmann's NASA (JPL) Laboratory
Contact information:
Dr. Gerard J. Holzmann
NASA/JPL Lab for Reliable Software
4800 Oak Grove Drive
Pasadena, CA 91109