Precise and Scalable Static Program Analysis of NASA Flight Software
- 1 January 2005
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 1095323X,p. 1-10
- https://doi.org/10.1109/aero.2005.1559604
Abstract
Recent NASA mission failures (e.g., Mars Polar Lander and Mars Orbiter) illustrate the importance of having an efficient verification and validation process for such systems. One software error, as simple as it may be, can cause the loss of an expensive mission, or lead to budget overruns and crunched schedules. Unfortunately, traditional verification methods cannot guarantee the absence of errors in software systems. Therefore, we have developed the CGS static program analysis tool, which can exhaustively analyze large C programs. CGS analyzes the source code and identifies statements in which arrays are accessed out of bounds, or, pointers are used outside the memory region they should address. This paper gives a high-level description of CGS and its theoretical foundations. It also reports on the use of CGS on real NASA software systems used in Mars missions (from Mars PathFinder to Mars Exploration Rover) and on the International Space StationKeywords
This publication has 10 references indexed in Scilit:
- Precise and efficient static array bound checking for large embedded C programsPublished by Association for Computing Machinery (ACM) ,2004
- A Scalable Nonuniform Pointer Analysis for Embedded ProgramsPublished by Springer Nature ,2004
- Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded SoftwarePublished by Springer Nature ,2002
- Ultra-fast aliasing analysis using CLAPublished by Association for Computing Machinery (ACM) ,2001
- Unification-based pointer analysis with directional assignmentsPublished by Association for Computing Machinery (ACM) ,2000
- Automatic analysis of pointer aliasing for untyped programsScience of Computer Programming, 1999
- Abstract Interpretation FrameworksJournal of Logic and Computation, 1992
- Constructive versions of Tarski’s fixed point theoremsPacific Journal of Mathematics, 1979
- Automatic discovery of linear restraints among variables of a programPublished by Association for Computing Machinery (ACM) ,1978
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpointsPublished by Association for Computing Machinery (ACM) ,1977