Presented By: Aerospace Engineering
Chair's Distinguished Lecture: Formal Methods in the Development of Highly Assured Software for Unmanned Aircraft Systems
Cesar Munoz NASA Research Computer Scientist
Cesar Munoz NASA Research Computer Scientist
In traditional software development methodologies, operational and functional requirements of systems are often specified in structured natural language notations. These restricted notations provide good documentation support, but only provide limited support for semantic analysis. These notations are generally not rich enough to unambiguously specify the requirements of safety-critical systems that, for example, involve complex numerical computations or that interact with the physical environment. Examples of these safety-critical systems are autonomous vehicles such as unmanned aircraft systems. This talk advocates the use of expressive formal logics, such as higher-order logic, to specify the operational and functional requirement of unmanned systems and to prove the correctness of these requirements. Semantic analysis of requirements written in higher-order logic is supported through the use of interactive theorem provers. Formal models serve as ideal reference implementations of functional requirements. Hence, formal logics enable software validation techniques where software implementations can be checked against functional requirements in a mechanical way. The Formal Methods group in the Safety-Critical Avionics Systems Branch at NASA Langley Research Center has conducted research on the development and application of formal verification techniques to safety-critical applications of interest to NASA for more than 30 years. This talk illustrates the use of formal methods at NASA Langley Research Center in the development of highly-assured autonomous unmanned aircraft systems.
About the Speaker...
Dr. Cesar Munoz is a senior research computer scientist at the NASA Langley Research Center, where he leads the Formal Methods Team. Dr. Munoz's primary research interest is the development of formal methods technology for the design, verification, and implementation of safety-critical aerospace systems. Dr. Munoz has contributed to the development of highly-assured software for the next generation of air traffic management concepts developed at NASA, including autonomous unmanned aircraft systems (UAS). In particular, Dr. Munoz is the main developer of DAIDALUS (Detect and Avoid Alerting Logic for Unmanned
Systems), a software library selected by RTCA SC-228 to be the reference implementation of detect and avoid minimum operational performance standards for UAS included in DO-365. Dr. Munoz is an internationally recognized expert on the computer science field of Formal Methods and has made several contributions to the development of interactive theorem proving technology for industrial
applications. Prior to joining NASA in 2009, Dr. Munoz was a Research Fellow at the National Institute of Aerospace. He got his Ph.D. degree in Computer Science from University of Paris 7, France, in 1997.
In traditional software development methodologies, operational and functional requirements of systems are often specified in structured natural language notations. These restricted notations provide good documentation support, but only provide limited support for semantic analysis. These notations are generally not rich enough to unambiguously specify the requirements of safety-critical systems that, for example, involve complex numerical computations or that interact with the physical environment. Examples of these safety-critical systems are autonomous vehicles such as unmanned aircraft systems. This talk advocates the use of expressive formal logics, such as higher-order logic, to specify the operational and functional requirement of unmanned systems and to prove the correctness of these requirements. Semantic analysis of requirements written in higher-order logic is supported through the use of interactive theorem provers. Formal models serve as ideal reference implementations of functional requirements. Hence, formal logics enable software validation techniques where software implementations can be checked against functional requirements in a mechanical way. The Formal Methods group in the Safety-Critical Avionics Systems Branch at NASA Langley Research Center has conducted research on the development and application of formal verification techniques to safety-critical applications of interest to NASA for more than 30 years. This talk illustrates the use of formal methods at NASA Langley Research Center in the development of highly-assured autonomous unmanned aircraft systems.
About the Speaker...
Dr. Cesar Munoz is a senior research computer scientist at the NASA Langley Research Center, where he leads the Formal Methods Team. Dr. Munoz's primary research interest is the development of formal methods technology for the design, verification, and implementation of safety-critical aerospace systems. Dr. Munoz has contributed to the development of highly-assured software for the next generation of air traffic management concepts developed at NASA, including autonomous unmanned aircraft systems (UAS). In particular, Dr. Munoz is the main developer of DAIDALUS (Detect and Avoid Alerting Logic for Unmanned
Systems), a software library selected by RTCA SC-228 to be the reference implementation of detect and avoid minimum operational performance standards for UAS included in DO-365. Dr. Munoz is an internationally recognized expert on the computer science field of Formal Methods and has made several contributions to the development of interactive theorem proving technology for industrial
applications. Prior to joining NASA in 2009, Dr. Munoz was a Research Fellow at the National Institute of Aerospace. He got his Ph.D. degree in Computer Science from University of Paris 7, France, in 1997.
Explore Similar Events
-
Loading Similar Events...
