Article
 

Establishing Flight Software Reliability: Testing, Model Checking, Constraint-Solving, Monitoring and Learning

Pubblico Deposited

Contenuto scaricabile

Scarica il pdf
https://ir.library.oregonstate.edu/concern/articles/d504rq91w

Descriptions

Attribute NameValues
Creator
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.
  • Keywords: Verification, Formal proof, Flight software, File systems, Model checking, Testing
Resource Type
DOI
Date Available
Date Issued
Citation
  • Groce, A., Havelund, K., Holzmann, G., Joshi, R., & Xu, R. G. (2014). Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning. Annals of Mathematics and Artificial Intelligence, 70(4), 315-349. doi:10.1007/s10472-014-9408-8
Journal Title
Journal Volume
  • 70
Journal Issue/Number
  • 4
Dichiarazione dei diritti
Funding Statement (additional comments about funding)
  • The research described in this publication was carried out at the Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration. Funding was also provided by NASA ESAS 6G.
Publisher
Peer Reviewed
Language
Replaces

Le relazioni

Parents:

This work has no parents.

Elementi

Thumbnail Titolo Data caricata Visibilità Azioni
file details GroceAlexElectricalEngineeringComputerScienceEstablishingFlightSoftware.pdf 2017-10-27 Pubblico Scaricare