FTSCS 2018
Sixth International Workshop on Formal Techniques for Safety-Critical Systems

(An ICFEM 2018 Satellite Event)

Gold Coast, Australia, November 16, 2018

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.

Naoki Kobayashi (the University of Tokyo)

On Two Higher-Order Extensions of Model Checking

Inspired by the success of finite state model checking in system verification, two kinds of its higher-order extensions have been studied since around 2000. One is model checking of higher-order recursion schemes (HORS), where the language for describing systems to be verified is extended to higher-order, and the other is higher-order fixpoint modal logic (HFL) model checking of finite-state systems, where the logic for specifying properties to be verified is extended to higher-order. The former has been successfully applied to automated verification of higher-order programs. In this talk, I will provide a gentle introduction to the HORS and HFL model checking problems, their applications to software verification, and the state-of-the-art of higher-order model checkers and tools built on top of them. I will also touch upon our recent result on the relationship between HORS and HFL model checking.

Short biography

Naoki Kobayashi was born in 1968, and received his B.S., M.S., and D.S. degrees from the University of Tokyo in 1991, 1993 and 1996, respectively. He is currently a professor in Department of Computer Science, Graduate School of Information Science and Technology, The University of Tokyo. His current major research interests are in principles of programming languages, especially type systems, higher-order model checking, and program verification.