This page is a rough timeline of “highlights” of my work at the SEI. A more complete listing of publications is on my research page.
2026
Probabilistic Verification to Support Next-Generation Certification
The Probabilistic Verification to Support Next-Generation Certification (ProVer-Cert) project examines the use of a formal, quantitative technique to establish confidence intervals on quantitative system properties. The goal is that this will support property-based (as opposed to process-based) certification approaches. The project is ongoing, but an overview of the tasking and early results is available.
I was an author on a technical report describing aspects of instantiating AADL’s Error-Modeling annex.
2025
Formalizing and Automating STPA with Robustness
The Formalizing and Automating STPA with Robustness (FASR) project uses formal methods to partially automate the third step of a hazard analysis technique called System-Theoretic Process Analysis (STPA). The talk linked above and accompanying poster were made partway through the project (so they lack some details) but I have a more detailed set of slides without video.
I was also an author on a technical report describing the semantics of AADL’s Error-Modeling annex.
2024
As part of the Assurance Evidence for Continuously-Evolving Real-Time Systems (ASERT) workgroup, I was an author on a paper describing how symbolic argumentation can support the analysis of an incident on a commercial flight.
2022-2023
Safety Analysis and Fault Detection Isolation and Recovery Synthesis for Time-Sensitive Cyber-Physical Systems
The Safety Analysis and Fault Detection Isolation and Recovery Synthesis for Time-Sensitive Cyber-Physical Systems (SAFIR) project is a three-year effort to study architecture-centric safety techniques for increasingly-autonomous cyber-physical systems. In addition to working on ASAP and the OSATE Slicer (see below), I have published papers with other team members on the use of contracts in system design and the generation of assurance argumentation from system requirements.
The OSATE Slicer: Graph-Based Reachability for Architectural Models
Many of the architectural analyses that run on AADL are fundamentally reachability queries. Prior work at K-State by Hari Thiagarajan demonstrated the utility of these queries; in this work I developed, evaluated, and benchmarked a highly-optimized query execution plugin that follows existing OSATE implementation patterns. You can read a summary of this work on the SEI Blog, or get the full details in the ECMFA23 publication, and download the supplementary files if you’re interested in re-running or extending the evaluation.
Architecture-Supported Audit Processor
One of the tasks I worked on in SAFIR (and ISSE, see below) is the Architecture-Supported Audit Processor or ASAP. ASAP is a software plugin for the OSATE workbench which presents safety-specific views of a system’s architecture. Installation instructions and source code are on the project’s github page, and you can read about the work in the ERTS22 publication.
2020-2021
Integrated Safety and Security Engineering
The Integrated Safety and Security Engineering (ISSE) project was a three-year effort looking at the degree to which safety engineering and security engineering can be harmonized when using architectural modeling tools like AADL. This
The AADL Error Library: An Operationalized Taxonomy of System Errors
The AADL Error Modelling Annex (EMV2, which was developed prior to this project) includes an Error Library. It both embeds a considerable amount of knowledge from academic research and industrial experience and is directly usable in AADL models. Peter Feiler and I wrote a a paper for the HILT18 workshop on the topic, produced a blog post, and made a podcast describing the effort.
2019
Guided Architecture Trade Space Exploration
I was the PI on a small research project looking at how user-guided exploration of what’s known as a system’s “trade space” might work. This work consists of extending OSATE to automatically explore potential design options in a system and then evaluate them using existing AADL analysis techniques. The code lives over on github, and you can watch a short presentation on the project, read a post on the SEI blog about the work, our 2021 paper from SoSyM, the 2019 paper from the MODELS conference, (or view the slides).
2017
Automated Analysis and Security Policy Enforcement
Automated Analysis and Security Policy Enforcement (AASPE) was a research project led by Julien Delange and Peter Feiler, and it began before I joined the SEI. It looked primarily at specifying and verifying the separation of different portions of a system (ie, keeping sensor data and control commands separate) as well as analyzing the impacts of potential attacks. I discussed this project, and other security aspects of AADL, in Episode 390 of the Software Engineering Radio Podcast.
SAFE and Secure
With my background in safety, I looked at safety and security co-analysis under the auspices of AASPE. The result of this effort was a SAW17 publication (slides here, also summarized in two blog posts) that describes some of the security applications of SAFE.