Ulgen: A Runtime Assurance Framework for Programming Safe Cyber-Physical Systems

Beyazit Yalcinkaya, Hazem Torfah, Ankush Desai, and Sanjit A. Seshia. Ulgen: A Runtime Assurance Framework for Programming Safe Cyber-Physical Systems. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, 42(11):3679–3692, 2023.

Download

[pdf] 

Abstract

We present Ulgen, a runtime assurance (RTA) framework for programming safe cyber–physical systems (CPSs). In Ulgen, a system is implemented as a collection of asynchronous processes executing RTA modules which are generalizations of the well-known Simplex architecture. An RTA module is composed of a set of safe controllers (SCs), designed to guarantee certain safety specifications, and a set of advanced controllers (ACs), optimized for performance, each defined to run under the specific conditions of the operating environment, and a decision module implementing the switching logic between the controllers. A source of complexity in achieving safe CPS is that these systems often involve concurrently interacting components with different execution semantics. To this end, Ulgen allows for the definition of RTA modules with either event-driven or time-driven execution semantics and encapsulates such components into RTA modules. It further provides primitives for implementing priority-based communication between asynchronous processes, which is a necessary feature for task prioritization mechanisms, such as contingency plans and interrupt service routines. The framework also provides formal guarantees on the safe execution of RTA modules based on a formal definition of well-formedness. In Ulgen, a well-formed RTA module combines SCs and ACs in a way that guarantees the underlying safety specifications assured by the SCs while delivering the desired performance offered by the ACs. We compare the safety guarantees of Ulgen against other state-of-the-art RTA frameworks and demonstrate its efficacy in implementing safe and performant CPS by presenting an extensive experimental evaluation of five case studies both in a simulation environment and on a real robotic platform.

BibTeX

@article{yalcinkaya-tcad23,
  author       = {Beyazit Yalcinkaya and
                  Hazem Torfah and
                  Ankush Desai and
                  Sanjit A. Seshia},
  title        = {{Ulgen}: {A} Runtime Assurance Framework for Programming Safe Cyber-Physical
                  Systems},
  journal      = {{IEEE} Transactions on Computer Aided Design of Integrated Circuits and Systems},
  volume       = {42},
  number       = {11},
  pages        = {3679--3692},
  year         = {2023},
  abstract  = {We present Ulgen, a runtime assurance (RTA) framework for programming safe cyber–physical systems (CPSs). In Ulgen, a system is implemented as a collection of asynchronous processes executing RTA modules which are generalizations of the well-known Simplex architecture. An RTA module is composed of a set of safe controllers (SCs), designed to guarantee certain safety specifications, and a set of advanced controllers (ACs), optimized for performance, each defined to run under the specific conditions of the operating environment, and a decision module implementing the switching logic between the controllers. A source of complexity in achieving safe CPS is that these systems often involve concurrently interacting components with different execution semantics. To this end, Ulgen allows for the definition of RTA modules with either event-driven or time-driven execution semantics and encapsulates such components into RTA modules. It further provides primitives for implementing priority-based communication between asynchronous processes, which is a necessary feature for task prioritization mechanisms, such as contingency plans and interrupt service routines. The framework also provides formal guarantees on the safe execution of RTA modules based on a formal definition of well-formedness. In Ulgen, a well-formed RTA module combines SCs and ACs in a way that guarantees the underlying safety specifications assured by the SCs while delivering the desired performance offered by the ACs. We compare the safety guarantees of Ulgen against other state-of-the-art RTA frameworks and demonstrate its efficacy in implementing safe and performant CPS by presenting an extensive experimental evaluation of five case studies both in a simulation environment and on a real robotic platform.},
}