TBA
Cesar Munoz (NASA Langley)
Formal Methods in the Development of Highly Assured Software for Unmanned Aircraft Systems
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 that involve, for example, the physical environment. This talk advocates 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, they enable the formal verification of complex numerically intensive algorithms and the rigorous validation of their implementations. The proposed approach is illustrated with two cases studies from NASA's research on Unmanned Aircraft Systems (UAS): Detect and Avoid Alerting Logic for Unmanned Systems (DAIDALUS) and Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS). DAIDALUS is the reference implementation of detect and avoid for UAS in FAA DO-365. ICAROUS is a software architecture built on top of DAIDALUS that enables the development of autonomous UAS applications.
Short Biography
Cesar Munoz got his M.Sc. and Ph.D. in Computer Science from the University of Paris 7. He then spent one and a half years at the Computer Science Laboratory at SRI International, before joining the Formal Methods group at ICASE -- NASA Langley in 1999. From 2003 to 2008, Munoz worked for the National Institute of Aerospace at Langley Research Center, where he led the NIA Formal Methods group. Munoz has been a Research Computer Scientist at NASA since 2009.
Munoz currently works on the development of formal methods technologies for NASA's Next Generation of Air Traffic Systems (NextGen), Validation and Verification of Flight Critical Systems (VVFCS), Unmanned Aircraft Systems Integration in the National Airspace System (UAS in the NAS), and Safe Autonomous Systems Operations (SASO) projects.