Abstract
Operational requirements of safety-critical systems are often written in restricted specification logics. These restricted logics are amenable to automated analysis techniques such as model-checking, but are not rich enough to express complex requirements of unmanned systems. This short paper advocates for the use of expressive logics, such as higher-order logic, to specify the complex operational requirements and safety properties of unmanned systems. These rich logics are less amenable to automation and, hence, require the use of interactive theorem proving techniques. However, these logics support the formal verification of complex requirements such as those involving the physical environment. Moreover, these logics enable validation techniques that increase confidence in the correctness of numerically intensive software. These features result in highly-assured software that may be easier to certify. The feasibility of this approach is illustrated with examples drawn for NASA’s unmanned aircraft systems.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Consiglio, M., Chamberlain, J., Muñoz, C., Hoffler, K.: Concept of integration for UAS operations in the NAS. In: Proceedings of 28th International Congress of the Aeronautical Sciences, ICAS 2012, Brisbane, Australia (2012)
Consiglio, M., Muñoz, C., Hagen, G., Narkawicz, A., Balachandran, S.: ICAROUS: integrated configurable algorithms for reliable operations of unmanned systems. In: Proceedings of the 35th Digital Avionics Systems Conference (DASC 2016), Sacramento, California, US, September 2016
Cook, S.P., Brooks, D., Cole, R., Hackenberg, D., Raska, V.: Defining well clear for unmanned aircraft systems. In: Proceedings of the 2015 AIAA Infotech@ Aerospace Conference, Number AIAA-2015-0481, Kissimmee, Florida, January 2015
Dutle, A.M., Muñoz, C.A., Narkawicz, A.J., Butler, R.W.: Software validation via model animation. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 92–108. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21215-9_6
FAA Sponsored Sense and Avoid Workshop. Sense and avoid (SAA) for Unmanned Aircraft Systems (UAS), October 2009
Fifarek, A.W., et al.: SpeAR v2.0: formalized past LTL specification and analysis of requirements. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 420–426. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_30
International Civil Aviation Organization (ICAO): Annex 2 to the Convention on International Civil Aviation, July 2005
Muñoz, C., Narkawicz, A.: Formal analysis of extended well-clear boundaries for unmanned aircraft. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 221–226. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_17
Muñoz, C., Narkawicz, A., Chamberlain, J.: A TCAS-II resolution advisory detection algorithm. In: Proceedings of the AIAA Guidance Navigation, and Control Conference and Exhibit 2013, Number AIAA-2013-4622, Boston, Massachusetts, August 2013
Muñoz, C., Narkawicz, A., Chamberlain, J., Consiglio, M., Upchurch, J.: A family of well-clear boundary models for the integration of UAS in the NAS. In: Proceedings of the 14th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, Number AIAA-2014-2412, Georgia, Atlanta, USA, June 2014
Muñoz, C., Narkawicz, A., Hagen, G., Upchurch, J., Dutle, A., Consiglio, M.: DAIDALUS: detect and avoid alerting logic for unmanned systems. In: Proceedings of the 34th Digital Avionics Systems Conference (DASC 2015), Prague, Czech Republic, September 2015
Narkawicz, A., Hagen, G.: Algorithms for collision detection between a point and a moving polygon, with applications to aircraft weather avoidance. In: 16th AIAA Aviation Technology, Integration, and Operations Conference, AIAA AVIATION Forum, Number AIAA-2016-3598, Washington, DC, USA, June 2016
Narkawicz, A., Muñoz, C., Dutle, A.: The MINERVA software development process. In: Proceedings of the Workshop on Automated Formal Methods 2017 (AFM 2017), Meno Park, California, USA (2017)
Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_217
RTCA SC-1228. RTCA-DO-365, Minimum Operational Performance Standards for Detect and Avoid (DAA) Systems, May 2017
RTCA SC-147. RTCA-DO-185B, Minimum Operational Performance Standards for Traffic alert and Collision Avoidance System II (TCAS II), July 2009
Siu, K., Moitra, A., Durling, M., Crapo, A., Li, M., Yu, H., Herencia-Zapana, H., Castillo-Effen, M., Sen, S., McMillan, C., Russell, D., Roy, S., Manolios, P.: Flight critical software and systems development using ASSERT. In: 2017 IEEE/AIAA 36th Digital Avionics Systems Conference (DASC), Number 978-1-5386-0365-9/17, pp. 1–10, September 2017
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 U.S. Government, as represented by the Administrator of the National Aeronautics and Space Administration. No copyright is claimed in the United States under Title 17, U.S. Code. All Other Rights Reserved.
About this paper
Cite this paper
Muñoz, C., Narkawicz, A., Dutle, A. (2018). From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds) Formal Methods. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_38
Download citation
DOI: https://doi.org/10.1007/978-3-319-95582-7_38
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-95581-0
Online ISBN: 978-3-319-95582-7
eBook Packages: Computer ScienceComputer Science (R0)