How can we reason about safety-critical systems, such as aircraft and spacecraft, to determine whether they behave safely? How can we formalize system requirements and enable automated specification debugging? How can we reason about large spaces of possible designs from the early system design phase? How can we carry through formal verification to runtime, enabling autonomous operation via intelligent, on-board system health management?

Our research addresses these questions and more, combining algorithms and techniques from symbolic model checking, runtime verification, control theory, probabilistic reasoning, and mathematical logic. The central theme of our innovations is a foundation in temporal logic.

Research Interests

  • Formal methods, verification and validation of safety-critical systems
  • Design-time checking of system logic and system requirements with applications in air traffic management, aerospace systems, automated control, biomedical privacy, secure protocols
  • System and safety health management for intelligent, autonomous Unmanned Aerial Systems (UAS)
  • Model checking, property-based design, model-based design
  • Linear Temporal Logic satisfiability checking, specification debugging techniques and theory
  • Automated reasoning, runtime monitoring, fault tolerance, safety analysis

Current Projects

Completed Projects

  • Intelligent Hardware-Enabled Sensor and Software Safety and Health Management for Autonomous UAS (NARI, 2013-2014)
    • NASA Aeronautics Research Mission Directorate (ARMD) Seedling Fund Phase I Award,
  • AG-4 (Air/Ground #4): Formal Methods Analysis for the Functional Allocation of the Next Generation Air Traffic Transportation System (NASA Airspace Systems Program, 2013-2014)
  • Verifi cation and Validation for Separation Assurance Algorithms (NASA Airspace Systems Program, 2008-2013)