Establishing flight software reliability: Testing, model checking, constraint-solving, monitoring and learning

Alex Groce, Klaus Havelund, Gerard Holzmann, Rajeev Joshi, Ru Gang Xu

Research output: Contribution to journalArticlepeer-review

20 Scopus citations

Abstract

In this paper we discuss the application of a range of techniques to the verification of mission-critical flight software at NASA's Jet Propulsion Laboratory. For this type of application we want to achieve a higher level of confidence than can be achieved through standard software testing. Unfortunately, given the current state of the art, especially when efforts are constrained by the tight deadlines and resource limitations of a flight project, it is not feasible to produce a rigorous formal proof of correctness of even a well-specified stand-alone module such as a file system (much less more tightly coupled or difficult-to-specify modules). This means that we must look for a practical alternative in the area between traditional testing and proof, as we attempt to optimize rigor and coverage. The approaches we describe here are based on testing, model checking, constraint-solving, monitoring, and finite-state machine learning, in addition to static code analysis. The results we have obtained in the domain of file systems are encouraging, and suggest that for more complex properties of programs with complex data structures, it is possibly more beneficial to use constraint solvers to guide and analyze execution (i.e., as in testing, even if performed by a model checking tool) than to translate the program and property into a set of constraints, as in abstraction-based and bounded model checkers. Our experience with non-file-system flight software modules shows that methods even further removed from traditional static formal methods can be assisted by formal approaches, yet readily adopted by test engineers and software developers, even as the key problem shifts from test generation and selection to test evaluation.

Original languageEnglish (US)
Pages (from-to)315-349
Number of pages35
JournalAnnals of Mathematics and Artificial Intelligence
Volume70
Issue number4
DOIs
StatePublished - Apr 2014
Externally publishedYes

Keywords

  • File systems
  • Flight software
  • Formal proof
  • Model checking
  • Testing
  • Verification

ASJC Scopus subject areas

  • Artificial Intelligence
  • Applied Mathematics

Fingerprint

Dive into the research topics of 'Establishing flight software reliability: Testing, model checking, constraint-solving, monitoring and learning'. Together they form a unique fingerprint.

Cite this