Research Interests
My main research interest is ensuring safety of
real-time and cyber-physical systems (CPS). Other interests, all related to the main one, include the application of
formal methods in design and verification of CPS, on-line monitoring of embedded and
cyber-physical systems and formal foundations for it, hybrid systems, automated
extraction of specifications from source code, and formal methods in software
engineering in general and in embedded software in particular. Although the word formal is repeated often in the previous sentence, I am more interested in exploring the boundary between formal and informal, and in carrying safety guarantees across the boundary, then in developing new formal techniques.
Please see my publications on these topics.
Besides several small things, I am currently involved in the following big
projects.
Dynamic assurance for autonomous systems with learning-based components
As part of the
DARPA Assured Autonomy program, we are exploring techniques for verification of cyber-physical systems that contain learning-based components, and generation of monitors that alert us when these components appear to be misbehaving. We are also studying construction of assurance cases for systems that rely on this monitoring.
Attack-resilient control systems
- The SPARCS project, part of the DARPA HACMS program, was exploring techniques to make control systems resilient to a variety of external attacks, including attacks on sensors that affect fidelity of sensor readings. We have also studied means of high-assurance implementation of resilient control designs. The HACMS program is over as of 2017.
- A follow-up project explores the concept of checkpointing and recovery for the control systems.
Modeling and analysis of medical devices and systems
- Generic Infusion Pump (GIP)
is a project to develop requirements for
infusion pumps and a reference implementation for such a pump. The
intent of the effort is to provide a platform for experimentation for the
academic embedded systems community.
- Medical device interoperability requires new approaches to safety analysis and regulatory approval. To support dynamically deployed multi-device clinical applications, we are developing an interoperability platform to provide isolation of different applications in terms of timing and quality of service. We are also exploring clinical applications that are enabled by medical device interoperability, including physiological closed-loop control.
- We are paticipating in the pacemaker challenge
Run-time Monitoring and Checking
The
Monitoring and
Checking project concentrates on run-time verification of
software systems. The MaC tool, which checks formally specified properties of
executions of Java applications, is one of the first runtime verification tools.
An on-going follow-up project, pursued jointly with BAE and funded by the DARPA BRASS program,
aims to apply runtime verification in the context of intent monitoring. The goal is to trigger
and guide dynamic adaptation of long-living software when intent deviations are detected.
As part of this project, we are developing a successor tool to MaC, which would fully support parametric monitoring and combination of synchronous and asynchronous monitors.
Resource interfaces for real-time systems
We have developed the notion of a component for the
construction and
compositional analysis of real-time systems. Components export
their resource requirements in order to allow modular composition that
preserves timing properties of the system. Component-based hierarchical schedulability analysis is supported by the tool
CARTS.
Architectural modeling of embedded systems.
We are developing tool support for the analysis of embedded systems
architectures expressed in the
AADL modeling
language. I am a member of the AADL standardization committee.
- We developed the Furness
toolset in collaboration with Fremont Associates, which includes an AADL
simulator and algorithms for formal schedulability analysis of AADL
models;
- We studied performance analysis of wireless architectures in a case
study performed in collaboration with Honeywell.
Quantitative trust management (QTM)
QTM is a novel
approach to access control under uncertainty combines credential-based
trust with reputation from past interactions. The project also
explores applications of reputation-based techniques
to
autonomous
system credibility
and
vandalism
detection. Funded by an ONR MURI.
A follow-up project applies QTM ideas to the area of crowd-sourced, model-based
manufacturing. We are building a flexible access control system from such an environment. Funded by the DARPA AVM program.
Modeling with hierarchical hybrid systems
The modeling environment is provided by the modeling language
CHARON and its
toolset. CHARON modeling approach has been extensively used in two domains:
- Modeling of embedded software, especially automotive controllers,
has been performed in the
MoBIES
(Model-Based Integration of Embedded Software) program
(over as of 1/04).
- Modeling of biological systems in the
BioComp
program (over as of 1/06).
HASTEN (High
Assurance Systems Tools and Environments) was
devoted to practical integration of different formal
methods and domain-specific specialization of formalisms.
MoBIES (Model Based
Integration of Embedded Systems) was a great DARPA project, which all
participants fondly remember.
My previous work in formal methods concentrated on the tools for formal
specification and verification, including
Concurrency Factory and
PARAGON. I was also
designing algorithms for different flavours of
model checking.
Conferences I am involved in (or was involved in recently)
- Cyber-Physical Systems Week, April 21-24, 2020 virtually in Sydney, Australia
- 20th International Conference on Runtime Verification, October 6-9, 2020, in Los Angeles, USA
- 18th International Symposium on Automated Technology for Verification and Analysis (ATVA), October 19-23, 2020, in Hanoi, Vietnam
Editorial duties