Generating Certification Evidence for Autonomous Unmanned Aircraft Using Model Checking and Simulation
- 1 May 2014
- journal article
- research article
- Published by American Institute of Aeronautics and Astronautics (AIAA) in Journal of Aerospace Information Systems
- Vol. 11 (5), 258-279
- https://doi.org/10.2514/1.i010096
Abstract
The use of unmanned aircraft for civil applications is expected to increase over the next decade, particularly in so-called dull, dirty, and dangerous missions. Unmanned aircraft will undoubtedly require some form of autonomy to ensure safe operations for all airspace users. However, to be used for civil applications, unmanned aircraft must gain regulatory approval in a process known as “certification”. This paper presents a proof-of-concept approach to the generation of certification evidence for autonomous unmanned aircraft based on a combination of formal verification and flight simulation. In particular, a class of autonomous systems controlled by rational agents is examined, and we give examples of 23 different properties, based on the rules of the air and notions of airmanship, which can be used in the formal model checking of rational agents controlling autonomous unmanned aircraft. Our techniques can be based on either 1) implicit models of the aircraft’s physical environment specified in terms of the range of sensor inputs the autonomous system may receive, or 2) more explicit physical models of the environment. Finally, we provide a description of how such formal verification can be used to refine the implementation of autonomous systems for unmanned aircraft.Keywords
This publication has 15 references indexed in Scilit:
- Verifying autonomous systemsCommunications of the ACM, 2013
- Towards Certification of Autonomous Unmanned Aircraft Using Formal Model Checking and SimulationPublished by American Institute of Aeronautics and Astronautics (AIAA) ,2012
- Certification of a Civil UAS: A Virtual Engineering ApproachPublished by American Institute of Aeronautics and Astronautics (AIAA) ,2011
- Model checking agent programming languagesAutomated Software Engineering, 2011
- An Introduction to Practical Formal Methods Using Temporal LogicPublished by Wiley ,2011
- Formal Methods for the Certification of Autonomous Unmanned Aircraft SystemsLecture Notes in Computer Science, 2011
- Satellite Control Using Rational Agent ProgrammingIEEE Intelligent Systems, 2010
- Space Shuttle Ground Processing with Monitoring AgentsIEEE Intelligent Systems, 2006
- Model Checking ProgramsAutomated Software Engineering, 2003
- Remote Agent: to boldly go where no AI system has gone beforeArtificial Intelligence, 1998