Transition-Based Robustness for Distributed and Cyber-Physical Systems

Transition-Based Robustness

Formal Verification

This project is motivated by the need to design software systems that are safe and robust. This project offers a transition-based definition of software robustness that complements the prior notion of behavioral robustness. Transition-based robustness identifies the safe environmental envelopes of a system with respect to a given safety property and normative environment. In our CAV’23 paper, we proposed transition-based robustness and used it to analyze cyber-physical systems. Currently, we are working to extend transition-based robustness to distributed protocols encoded in the TLA+ formal specification language.

Publications:

• Safe Environmental Envelopes of Discrete Systems