Article

Modeling and verification of an air traffic concept of operations

Authors:

César A. Muñoz,

Gilles Dowek,

Víctor CarreñoAuthors Info & Claims

ISSTA '04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis

Pages 175 - 182

https://doi.org/10.1145/1007512.1007536

Published: 01 July 2004 Publication History

Get Access

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.]]

Google Scholar

[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.]]

Google Scholar

[3]

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99), volume 1579 of Lecture Notes in Computer Science, pages 193--207. Springer, 1999.]]

Digital Library

Google Scholar

[4]

J. R. Burch, E. M. Clarke, and K. L. McMillan. Symbolic model checking: $10^20$ states and beyond. Information and Computation, 98:142--170, 1992.]]

Digital Library

Google Scholar

[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.]]

Google Scholar

[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.]]

Google Scholar

[7]

Federal Aviation Regulations/Aeronautical Information Manual, 1999.]]

Google Scholar

[8]

G. J. Holzmann. The SPIN Model Checker, Primer and Reference Manual. Addison-Wesley, 2003.]]

Digital Library

Google Scholar

[9]

S. P. Office. Small Aircraft Transportation System Program Plan. NASA Langley Research Center, http://sats.larc.nasa.gov/main.html, 2001.]]

Google Scholar

[10]

S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748--752, Saratoga, NY, June 1992. Springer-Verlag.]]

Digital Library

Google Scholar

[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.]]

Google Scholar

[12]

O. Shtrichman. Tuning SAT checkers for Bounded Model Checking. In Computer Aided Verification, 12th International Conference, CAV 2000, volume 1855 of Lecture Notes in Computer Science, pages 480--494. Springer, 2000.]]

Digital Library

Google Scholar

Cited By

View all

Prabhakar PDuggirala PMitra SViswanathan M(2015)Hybrid automata-based CEGAR for rectangular hybrid systemsFormal Methods in System Design10.1007/s10703-015-0225-446:2(105-134)Online publication date: 28-Feb-2015
https://doi.org/10.1007/s10703-015-0225-4
Liu DFulton NZic Jde Groot M(2013)Verifying an Aircraft Proximity Characterization Method in CoqFormal Methods and Software Engineering10.1007/978-3-642-41202-8_7(86-101)Online publication date: 2013
https://doi.org/10.1007/978-3-642-41202-8_7
Prabhakar PDuggirala PMitra SViswanathan M(2013)Hybrid Automata-Based CEGAR for Rectangular Hybrid SystemsProceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 773710.1007/978-3-642-35873-9_6(48-67)Online publication date: 20-Jan-2013
https://dl.acm.org/doi/10.1007/978-3-642-35873-9_6
Show More Cited By

Index Terms

Modeling and verification of an air traffic concept of operations
1. Computing methodologies
  1. Symbolic and algebraic manipulation
2. Theory of computation
  1. Logic

Recommendations

Modeling and verification of an air traffic concept of operations

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 ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...

Comments

Information & Contributors

Information

Published In

ISSTA '04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis

July 2004

294 pages

ISBN:1581138202

DOI:10.1145/1007512

General Chair:
George Avrunin
University of Massachusetts, USA
,
Program Chair:
Gregg Rothermel
University of Nebraska -- Lincoln, USA

ACM SIGSOFT Software Engineering Notes Volume 29, Issue 4
July 2004
284 pages
ISSN:0163-5948
DOI:10.1145/1013886
Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ISSTA04

Sponsor:

ISSTA04: International Symposium on Software Testing and Analysis 2004

July 11 - 14, 2004

Massachusetts, Boston, USA

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
519
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Prabhakar PDuggirala PMitra SViswanathan M(2015)Hybrid automata-based CEGAR for rectangular hybrid systemsFormal Methods in System Design10.1007/s10703-015-0225-446:2(105-134)Online publication date: 28-Feb-2015
https://doi.org/10.1007/s10703-015-0225-4
Liu DFulton NZic Jde Groot M(2013)Verifying an Aircraft Proximity Characterization Method in CoqFormal Methods and Software Engineering10.1007/978-3-642-41202-8_7(86-101)Online publication date: 2013
https://doi.org/10.1007/978-3-642-41202-8_7
Prabhakar PDuggirala PMitra SViswanathan M(2013)Hybrid Automata-Based CEGAR for Rectangular Hybrid SystemsProceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 773710.1007/978-3-642-35873-9_6(48-67)Online publication date: 20-Jan-2013
https://dl.acm.org/doi/10.1007/978-3-642-35873-9_6
Consiglio MCarreno VWilliams DMunoz C(2012)Conflict Prevention and Separation Assurance in the Small Aircraft Transportation SystemAIAA 5th ATIO and16th Lighter-Than-Air Sys Tech. and Balloon Systems Conferences10.2514/6.2005-7463Online publication date: 19-Jun-2012
https://doi.org/10.2514/6.2005-7463
Carreno VMunoz C(2012)Safety Verification of the Small Aircraft Transportation System Concept of OperationsAIAA 5th ATIO and16th Lighter-Than-Air Sys Tech. and Balloon Systems Conferences10.2514/6.2005-7423Online publication date: 19-Jun-2012
https://doi.org/10.2514/6.2005-7423
Baxley BWilliams DConsiglio MAdams CAbbott T(2012)The Small Aircraft Transportation System, Higher Volume Operations Concept and Research SummaryAIAA 5th ATIO and16th Lighter-Than-Air Sys Tech. and Balloon Systems Conferences10.2514/6.2005-7379Online publication date: 19-Jun-2012
https://doi.org/10.2514/6.2005-7379
Cheng ANiktab HWalston M(2012)Timing Analysis of Small Aircraft Transportation System (SATS)2012 IEEE International Conference on Embedded and Real-Time Computing Systems and Applications10.1109/RTCSA.2012.46(58-67)Online publication date: Aug-2012
https://doi.org/10.1109/RTCSA.2012.46
Oberheid HSöffker D(2008)Cooperative Arrival Management in Air Traffic Control - A Coloured Petri Net Model of Sequence PlanningProceedings of the 29th international conference on Applications and Theory of Petri Nets10.1007/978-3-540-68746-7_23(348-367)Online publication date: 23-Jun-2008
https://dl.acm.org/doi/10.1007/978-3-540-68746-7_23
Akgunduz AJaumard BMoeini G(2018)Deconflicted Air-Traffic Planning With Speed-Dependent Fuel-Consumption FormulationIEEE Transactions on Intelligent Transportation Systems10.1109/TITS.2017.274235919:6(1890-1901)Online publication date: Jun-2018
https://doi.org/10.1109/TITS.2017.2742359
Sardar MAfaq NHasan OHoque K(2018)Towards Probabilistic Formal Analysis of SATS-Simultaneously Moving Aircraft (SATS-SMA)Journal of Automated Reasoning10.1007/s10817-017-9416-660:1(85-105)Online publication date: 1-Jan-2018
https://dl.acm.org/doi/10.1007/s10817-017-9416-6
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Index Terms

Recommendations