Modeling and verification of an air traffic concept of operations

ABSTRACT

A high level model of the concept of operations of NASA's Small Aircraft Transportation System for Higher Volume Operations (SATS-HVO) is presented. The model is a non-deterministic, asynchronous transition system. It provides a robust notion of safety that relies on the logic of the concept rather than on physical constraints such as aircraft performances. Several safety properties were established on this model. The modeling and verification effort resulted in the identification of 9 issues, including one major flaw, in the original concept. Ten recommendations were made to the SATS-HVO concept development working group. All the recommendations were accepted and incorporated into the current concept of operations. The model was written in PVS. The verification is performed using an explicit state exploration algorithm written and proven correct in PVS.

REFERENCES

• 1: C. Adams, M. Consiglio, K. Jones, and D. Williams. SATS HVO Operational Concept: Nominal Operations. NASA Langley Research Center, 2003.
• 2: S. Bensalem, V. Ganesh, Y. Lakhnech, C. Muñoz, S. Owre, H. Rueß, J. Rushby, V. Rusu, H. Saïdi, N. Shankar, E. Singerman, and A. Tiwari. An overview of SAL. Technical Report NASA/CP-2000-210100, NASA Langley Research Center, Hampton, Virginia, June 2000.
• 3: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 4: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 5: L. de Moura, S. Owre, and N. Shankar. The SAL language manual. Technical Report SRI-CSL-01-01 (Rev. 2), SRI International, August 2003. Available at: http://sal.csl.sri.com.
• 6: G. Dowek, C. Muñoz, and V. Carreño. Abstract model of the SATS concept of operations: Initial results and recommendations. Technical Report NASA/TM-2004-213006, NASA Langley Research Center, NASA LaRC,Hampton VA 23681-2199, USA, March 2004.
• 7: Federal Aviation Regulations/Aeronautical Information Manual, 1999.
• 8: G. J. Holzmann. The SPIN Model Checker, Primer and Reference Manual. Addison-Wesley, 2003.
• 9: S. P. Office. Small Aircraft Transportation System Program Plan. NASA Langley Research Center, http://sats.larc.nasa.gov/main.html, 2001.
• 10: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 11: N. Shankar. Efficiently executing PVS. Project report, Computer Science Laboratory, SRI International, Menlo Park, CA, Nov. 1999. Available at http://www.csl.sri.com/shankar/PVSeval.ps.gz.
• 12: Ofer Shtrichman, Tuning SAT Checkers for Bounded Model Checking, Proceedings of the 12th International Conference on Computer Aided Verification, p.480-494, July 15-19, 2000

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION

General Terms:
Reliability, Verification

Keywords:
air traffic management systems, model checking, theorem proving