Skip to main content
Search
Search
Quick Search anywhere
Quick Search fdjslkfh
Advanced search
Cart
Join AIAA Institution Login
Skip main navigationClose Drawer MenuOpen Drawer Menu
Journal of Aerospace Information Systems logo
No AccessFull-Length Paper

Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges

Published Online:7 Nov 2014https://doi.org/10.2514/1.I010178

Abstract

Complex software systems are becoming increasingly prevalent in aerospace applications: in particular, to accomplish critical tasks. Ensuring the safety of these systems is crucial, as they can have subtly different behaviors under slight variations in operating conditions. This paper advocates the use of formal verification techniques and in particular theorem proving for hybrid software-intensive systems as a well-founded complementary approach to the classical aerospace verification and validation techniques, such as testing or simulation. As an illustration of these techniques, a novel lateral midair collision-avoidance maneuver is studied in an ideal setting, without accounting for the uncertainties of the physical reality. The challenges that naturally arise when applying such technology to industrial-scale applications is then detailed, and proposals are given on how to address these issues.

References

  • [1] Trimble S., “AUVSI: RQ-7 Likely Not to Blame for C-130 Collision,” Flight Daily News, Aug. 2011. Google Scholar

  • [2] Johnson C., “Review of the BFU Überlingen Accident Report,” Dept. of Computing Science, Univ. of Glasgow, Glasgow, Scotland, 2004, www.dcs.gla.ac.uk/~johnson/Eurocontrol/Ueberlingen/Ueberlingen_Final_Report.PDF [retrieved Sept. 2014]. Google Scholar

  • [3] Weiss K. A., Dulac N., Chiesi S., Daouk M., Zipkin D. and Leveson N., “Engineering Spacecraft Mission Software Using a Model-Based and Safety-Driven Design Methodology,” Journal of Aerospace Computing, Information, and Communication, Vol. 3, No. 11, 2006, pp. 562–586. doi:https://doi.org/10.2514/1.24677 1542-9423 LinkGoogle Scholar

  • [4] Fix L., “Fifteen Years of Formal Property Verification in Intel,” 25 Years of Model Checking, edited by Grumberg O. and Veith H., Springer–Verlag, Berlin, 2008, pp. 139–144. CrossrefGoogle Scholar

  • [5] Delmas D. and Souyris J., “Astrée: From Research to Industry,” Static Analysis: Lecture Notes in Computer Science, Vol. 4634, edited by Nielson H. and Filé G., Springer–Verlag, Berlin, 2007, pp. 437–451. CrossrefGoogle Scholar

  • [6] Bertrane J., Cousot P., Cousot R., Feret J., Mauborgne L., Miné A. and Rival X., “Static Analysis and Verification of Aerospace Software by Abstract Interpretation,” AIAA [email protected] 2010, AIAA Paper  2010-3385, 2010. LinkGoogle Scholar

  • [7] Platzer A., “Differential Dynamic Logic for Hybrid Systems,” Journal of Automated Reasoning, Vol. 41, No. 2, 2008, pp. 143–189. doi:https://doi.org/10.1007/s10817-008-9103-8 JAREEW 0168-7433 CrossrefGoogle Scholar

  • [8] Platzer A., “Logics of Dynamical Systems,” Logic in Computer Science (LICS’12), IEEE, Piscataway, NJ, 2012, pp. 13–24. Google Scholar

  • [9] Platzer A. and Clarke E. M., “Computing Differential Invariants of Hybrid Systems As Fixedpoints,” Computer Assisted Verification: Lecture Notes in Computer Science, Vol. 5123, edited by Gupta A. and Malik S., Springer–Verlag, Berlin, 2008, pp. 176–189. CrossrefGoogle Scholar

  • [10] Henzinger T. A., “The Theory of Hybrid Automata,” Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, IEEE, Piscataway, NJ, 1996, pp. 278–292. Google Scholar

  • [11] Platzer A., Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer–Verlag, Heidelberg, 2010. CrossrefGoogle Scholar

  • [12] Platzer A. and Quesel J.-D., “KeYmaera: A Hybrid Theorem Prover for Hybrid Systems,” Automated Reasoning: Lecture Notes in Computer Science, Vol. 5195, edited by Armando A., Baumgartner P. and Dowek G., Springer–Verlag, Berlin, 2008, pp. 171–178. CrossrefGoogle Scholar

  • [13] Loos S. M., Platzer A. and Nistor L., “Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified,” Formal Methods: Lecture Notes in Computer Science, Vol. 6664, Springer–Verlag, Berlin, 2011, pp. 42–56. CrossrefGoogle Scholar

  • [14] Loos S. M. and Platzer A., “Safe Intersections: At the Crossing of Hybrid Systems and Verification,” Intelligent Transportation Systems (ITSC’11), edited by Yi K., IEEE, Piscataway, NJ, 2011, pp. 1181–1186. doi:https://doi.org/10.1109/ITSC.2011.6083138 CrossrefGoogle Scholar

  • [15] Mitsch S., Loos S. M. and Platzer A., “Towards Formal Verification of Freeway Traffic Control,” Proceedings of the 2nd International Conference on Cyber-Physical Systems (ICCPS’12), edited by Lu C., IEEE, Piscataway, NJ, 2012, pp. 171–180. CrossrefGoogle Scholar

  • [16] Platzer A. and Quesel J.-D., “European Train Control System: A Case Study in Formal Verification,” Formal Engineering Methods: Lecture Notes in Computer Science, Vol. 5885, edited by Breitman K. and Cavalcanti A., Springer–Verlag, Berlin, 2009, pp. 246–265. CrossrefGoogle Scholar

  • [17] Platzer A. and Clarke E. M., “Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study,” Formal Methods: Lecture Notes in Computer Science, Vol. 5850, edited by Cavalcanti A. and Dams D., Springer–Verlag, Berlin, 2009, pp. 547–562. CrossrefGoogle Scholar

  • [18] Loos S. M., Renshaw D. W. and Platzer A., “Formal Verification of Distributed Aircraft Controllers,” Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC’13), edited by Belta C. and Ivancic F., ACM, Philadelphia, April 2013, pp. 125–130. Google Scholar

  • [19] Mitsch S., Ghorbal K. and Platzer A., “On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles,” Robotics: Science and Systems IX, edited by Newman P., Fox D. and Hsu D., Technische Universität Berlin, Berlin, June 2013, http://www.roboticsproceedings.org/rss09/p14.pdf [retrieved Sept. 2014]. Google Scholar

  • [20] Kouskoulas Y., Renshaw D. W., Platzer A. and Kazanzides P., “Certifying the Safe Design of a Virtual Fixture Control Algorithm for a Surgical Robot,” Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC’13), edited by Belta C. and Ivancic F., ACM, Philadelphia, April 2013, pp. 263–272. Google Scholar

  • [21] Dubins L. E., “On Curves of Minimal Length with a Constraint on Average Curvature, and with Prescribed Initial and Terminal Positions and Tangents,” American Journal of Mathematics, Vol. 79, No. 3, 1957, pp. 497–516. doi:https://doi.org/10.2307/2372560 AJMAAN 0002-9327 CrossrefGoogle Scholar

  • [22] Bicchi A., Marigo A., Pappas G., Pardini M., Parlangeli G., Tomlin C. and Sastry S., “Decentralized Air Traffic Management Systems: Performance and Fault Tolerance,” Proceedings of the IFAC International Workshop on Motion Control (MC’98), The International Federation of Automatic Control, 1998, pp. 259–264. Google Scholar

  • [23] Tomlin C., Pappas G. J. and Sastry S., “Conflict Resolution for Air Traffic Management: A Study in Multi-Agent Hybrid Systems,” IEEE Transactions on Automatic Control, Vol. 43, No. 4, 1998, pp. 509–521. doi:https://doi.org/10.1109/9.664154 IETAA9 0018-9286 CrossrefGoogle Scholar

  • [24] Platzer A., “Differential-Algebraic Dynamic Logic for Differential-Algebraic Programs,” Journal of Logic and Computation, Vol. 20, No. 1, 2010, pp. 309–352. doi:https://doi.org/10.1093/logcom/exn070 JLCOEU CrossrefGoogle Scholar

  • [25] Ghorbal K. and Platzer A., “Characterizing Algebraic Invariants by Differential Radical Invariants,” Tools and Algorithms for the Construction and Analysis of Systems: Lecture Notes in Computer Science, Vol. 8413, edited by Ábrahám E. and Havelund K., Springer–Verlag, Berlin, 2014, pp. 279–294. CrossrefGoogle Scholar

  • [26] Platzer A, “Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs,” Automated Deduction: Lecture Notes in Computer Science, Vol. 6803, edited by Bjørner N. and Sofronie-Stokkermans V., Springer–Verlag, Berlin, 2011, pp. 431–445. CrossrefGoogle Scholar

  • [27] Kalman R. E., “A New Approach to Linear Filtering and Prediction Problems,” Journal of Basic Engineering, Vol. 82, No. 1, 1960, pp. 35–45. doi:https://doi.org/10.1115/1.3662552 JBAEAI 0021-9223 CrossrefGoogle Scholar

  • [28] Kochenderfer M. J., Holland J. E. and Chryssanthacopoulos J. P., “Next-Generation Airborne Collision Avoidance System,” Lincoln Laboratory Journal, Vol. 19, No. 1, 2012, pp. 17–33, https://www.ll.mit.edu/publications/journal/pdf/vol19_no1/19_1_1_Kochenderfer.pdf [retrieved Sept. 2014]. LLJ0EJ 0896-4130 Google Scholar

  • [29] Puterman M. L., Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, Hoboken, NJ, 2009. Google Scholar

  • [30] von Essen C. and Giannakopoulou D., “Analyzing the Next Generation Airborne Collision Avoidance System,” Tools and Algorithms for the Construction and Analysis of Systems: Lecture Notes in Computer Science, Vol. 8413, edited by Ábrahám E. and Havelund K., Springer–Verlag, Berlin, 2014, pp. 620–635. CrossrefGoogle Scholar

  • [31] Mitsch S. and Platzer A., “ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models,” Runtime Verification: Lecture Notes in Computer Science, Vol. 8734, edited by Bonakdarpour B. and Smolka S. A., Springer–Verlag, Berlin, 2014, pp. 199–214. CrossrefGoogle Scholar

  • [32] Bouissou O., Goubault E., Putot S., Tekkal K. and Vedrine F., “HybridFluctuat: A Static Analyzer of Numerical Programs Within a Continuous Environment,” Computer Aided Verification: Lecture Notes in Computer Science, Springer–Verlag, Berlin, 2009, pp. 620–626. CrossrefGoogle Scholar

  • [33] Venet A, “The Gauge Domain: Scalable Analysis of Linear Inequality Invariants,” Computer Aided Verification: Lecture Notes in Computer Science, Vol. 7358, edited by Madhusudan P. and Seshia S., Springer–Verlag, Berlin, 2012, pp. 139–154. CrossrefGoogle Scholar

  • [34] Bellman R. E., Dynamic Programming, Princeton Univ. Press, Princeton, NJ, 1962. Google Scholar

  • [35] “Software Considerations in Airborne Systems and Equipment Certification,” RTCA STD DO-178C, Washington, D.C., 2012. Google Scholar

  • [36] Miller S. P., Whalen M. W. and Cofer D. D., “Software Model Checking Takes Off,” Communications of the ACM, Vol. 53, No. 2, 2010, pp. 58–64. doi:https://doi.org/10.1145/1646353 CACMA2 0001-0782 CrossrefGoogle Scholar

  • [37] Souyris J., Wiels V., Delmas D. and Delseny H., “Formal Verification of Avionics Software Products,” Formal Methods: Lecture Notes in Computer Science, Vol. 5850, edited by Cavalcanti A. and Dams D., Springer–Verlag, Berlin, 2009, pp. 532–546. CrossrefGoogle Scholar

  • [38] Kuchar J. K. and Yang L. C., “A Review of Conflict Detection and Resolution Modeling Methods,” IEEE Transactions on Intelligent Transportation Systems, Vol. 1, No. 4, 2000, pp. 179–189. doi:https://doi.org/10.1109/6979.898217 CrossrefGoogle Scholar

  • [39] Dowek G., Muñoz C. and Carreño V. A., “Provably Safe Coordinated Strategy for Distributed Conflict Resolution,” 2005 AIAA Guidance Navigation, and Control Conference and Exhibit, AIAA Paper  2005-6047, 2005. LinkGoogle Scholar

  • [40] Galdino A. L., Muñoz C. and Ayala-Rincón M., “Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm,” Logic, Language, Information and Computation: Lecture Notes in Computer Science, Vol. 4576, edited by Leivant D. and de Queiroz R., Springer–Verlag, Berlin, 2007, pp. 177–188. CrossrefGoogle Scholar

  • [41] Platzer A. and Clarke E. M., “Computing Differential Invariants of Hybrid Systems As Fixedpoints,” Formal Methods in System Design, Vol. 35, No. 1, 2009, pp. 98–120. doi:https://doi.org/10.1007/s10703-009-0079-8 FMSDE6 0925-9856 CrossrefGoogle Scholar

  • [42] Prandini M., Hu J., Lygeros J. and Sastry S., “A Probabilistic Approach to Aircraft Conflict Detection,” IEEE Transactions on Intelligent Transportation Systems, Vol. 1, No. 4, 2000, pp. 199–220. doi:https://doi.org/10.1109/6979.898224 CrossrefGoogle Scholar

  • [43] Lygeros J. and Prandini M., “Aircraft and Weather Models for Probabilistic Collision Avoidance in Air Traffic Control,” Proceedings of the 41st IEEE Conference on Decision and Control, Vol. 3, IEEE, Piscataway, NJ, 2002, pp. 2427–2432. Google Scholar

  • [44] Lachner R., “Collision Avoidance as a Differential Game: Real-Time Approximation of Optimal Strategies Using Higher Derivatives of the Value Function,” IEEE International Conference on Systems, Man, and Cybernetics, 1997. Computational Cybernetics and Simulation, 1997, Vol. 3, IEEE, Piscataway, NJ, 1997, pp. 2308–2313. Google Scholar

  • [45] Bilimoria K. D., Lee H. Q., Mao Z.-H. and Feron E., “Comparison of Centralized and Decentralized Conflict Resolution Strategies for Multiple-Aircraft Problems,” AIAA Guidance, Navigation, and Control Conference, AIAA Paper  2000-4268, 2000. LinkGoogle Scholar

  • [46] Hwang I. and Tomlin C., “Protocol-Based Conflict Resolution for Air Traffic Control,” Air Traffic Control Quarterly, Vol. 15, No. 1, 2007, pp. 1–34. ATCQER 1064-3818 LinkGoogle Scholar

  • [47] Mitchell I. M., Bayen A. M. and Tomlin C. J., “A Time-Dependent Hamilton-Jacobi Formulation of Reachable Sets for Continuous Dynamic Games,” IEEE Transactions on Automatic Control, Vol. 50, No. 7, 2005, pp. 947–957. doi:https://doi.org/10.1109/TAC.2005.851439 IETAA9 0018-9286 CrossrefGoogle Scholar

  • [48] Frehse G., Guernic C. L., Donzé A., Cotton S., Ray R., Lebeltel O., Ripado R., Girard A., Dang T. and Maler O., “SpaceEx: Scalable Verification of Hybrid Systems,” Computer Aided Verification: Lecture Notes in Computer Science, Vol. 6806, edited by Gopalakrishnan G. and Qadeer S., Springer–Verlag, Berlin, 2011, pp. 379–395. CrossrefGoogle Scholar

  • [49] Umeno S. and Lynch N. A., “Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study,” Formal Methods: Lecture Notes in Computer Science, Vol. 4085, edited by Misra J., Nipkow T. and Sekerinski E., Springer–Verlag, Berlin, 2006, pp. 64–80. CrossrefGoogle Scholar

  • [50] Umeno S. and Lynch N. A., “Safety Verification of an Aircraft Landing Protocol: A Refinement Approach,” Hybrid Systems: Computation, and Control: Lecture Notes in Computer Science, Vol. 4416, edited by Bemporad A., Bicchi A. and Buttazzo G., Springer–Verlag, Berlin, 2007, pp. 557–572. CrossrefGoogle Scholar

  • [51] Bayen A. M., Mitchell I. M., Osihi M. K. and Tomlin C. J., “Aircraft Autolander Safety Analysis Through Optimal Control-Based Reach Set Computation,” Journal of Guidance, Control, and Dynamics, Vol. 30, No. 1, 2007, pp. 68–77. doi:https://doi.org/10.2514/1.21562 JGCDDT 0162-3192 LinkGoogle Scholar

Previous article
Next article