Introduction

The application of model checking to the DEOS real-time embedded aerospace operating system from Honeywell discovered a subtle error not uncovered using the testing techniques required for FAA certification. The impact of this error during flight could have been starvation of critical real-time flight calculations.

Presentations

• Guillaume Brat, Dimitra Giannakopoulou, Klaus Havelund, Michael Lowry, Phil Oh, Corina Pasareanu, Charles Pecheur, John Penix, Willem Visser, Matthew Dwyer, John Hatcliff, Alex Groce, Flavia Lerda, "Software Model Checking," NASA Ames Automated Software Engineering Group, 2002.
  [Presentations (Powerpoint, 512K),(PDF, 1.7M)]
  [Highlights (Powerpoint, 369K),(PDF, 134K)]

Publications

Klaus Havelund, Grigore Rosu, "Monitoring Programs using Rewriting,"Proc. ASE'01: 16th Int'l Conf. on Automated Software Engineering, Coronado Island, CA., pp. 135-143, Nov. 26-29, 2001.
[papers (PDF, 112K)]

Flavio Lerda, Willem Visser, "Addressing Dynamic Issues of Program Model Checking," Proc. SPIN 2001: 8th Int'l SPIN Workshop on Model Checking of Software, Springer LNCS, vol. 2057, Toronto, Canada, pp. 80-102, May 19-20, 2001.
[papers (PDF, 244K)]

Corina Pasareanu, Matthew Dwyer, Willem Visser, "Finding Feasible Abstract Counter-examples," Int'l Journal on Software Tools for Technology Transfer, Springer LNCS, vol. 5, no. 1, pp. 34-48, Nov. 2003.

Guillaume Brat, Klaus Havelund, SeungJoon Park, Willem Visser, "Model Checking Programs," Proc. ASE'00: 15th IEEE Int'l Conf. on Automated Software Engineering, Grenoble, France, pp. 3-11, Sep. 11-15, 2000.
[papers (PDF, 70K),(Postscript, 111k)]

William Visser, SeungJoon Park, John Penix, "Using Predicate Abstraction to Reduce Object-Oriented Programs for Model Checking," Proc. FMSP'00: 3rd ACM Workshop on Formal Methods in Software Practice, Portland, OR., pp. 3-13, Aug. 23-25, 2000.
[papers (PDF, 163K),(Postscript, 236K)]-->

Corina Pasareanu, "DEOS Kernel: Environment Modeling using LTL Assumptions," NASA Ames Technical Report #NASA-ARC-IC-2000-196, July 2000.
[papers (PDF, 154K)]

James Corbett, Matthew Dwyer, Hohn Hatcliff, Corina Pasareanu, Robby, Shawn Lauback, Hongjun Zheng, "Bandera: Extracting Finite-State Models from Java Source Code," Proc. ICSE 2000: 22nd Int'l Conf. on Software Engineering, Limerick, Ireland, pp. 439-448, June 4-11, 2000.
[paper (PDF, 1.7M)]

John Penix, Willem Visser, Eric Engstrom, Aaron Larson, Nicholas Weininger, "Verification of Time Partitioning in the DEOS Scheduler Kernel," Proc. 22nd Int'l Conf. on Software Engineering, Limerick, Ireland, pp. 488-497, June 2000.
[papers (PDF, 74K)]

Klaus Havelund, Michael Lowry, SeungJoon Park, Charles Pecheur, John Penix, Willem Visser, Jonathan White, "Formal Analysis of the Remote Agent Before and After Flight," Proc. 5th NASA Langley Formal Methods Workshop, Williamsburg, VA., June 2000.
[papers (PDF, 97K)]

Matthew Dwyer, John Hatcliff, Robby Joehanes, Shawn Laubach, Corina Pasareanu, Robby, Willem Visser, and Hongjun Zheng, "Tool-Supported Program Abstraction for Finite-State Verification," Proc. ICSE 2001: 23rd Int'l Conf. on Software Engineering, Toronto, Canada, pp. 177-187, May 12-19, 2001. [paper (PDF, 99K)]

Willem Visser, Klaus Havelund, John Penix, "Adding Active Objects to SPIN," Proc. 5th Int'l SPIN Workshop on Theoretical Aspects of Model Checking, Trento, Italy, pp. 40-51, July 5, 1999.
[papers (PDF, 196K)]

Klaus Havelund, Tom Pressburger, "Model Checking Java Programs Using Java PathFinder," Int'l Journal on Software Tools for Technology Transfer, vol. 2, no. 4, pp. 366-381, Apr. 2000.
[papers (PDF, 298K)]

Last modified: Oct. 31, 2008 by Allen Dutra.