Research
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
Software
- Software for generating the de facto Industry Standard Benchmarks for LTL Model Checkers and LTL Satisfiability Checkers
- PANDA (Portfolio Approach to Navigating the Design of Automata)
- Software for SystemC Monitors: CHIMP (CHIMP Handles Instrumentation for Monitoring of Properties)
- Realizable Responsive Unobtrusive Unit (R2U2)
