# A Component-Based Simplex Architecture for High-Assurance Cyber-Physical Systems

## TL;DR

The paper introduces a Component-Based Simplex Architecture (CBSA) that combines assume-guarantee reasoning with the Simplex control framework to ensure runtime safety of component-based cyber-physical systems, enabling advanced controllers while guaranteeing safety properties.

## Contribution

It presents a novel compositional framework integrating A-G reasoning with Simplex, allowing scalable safety assurance and formal proofs for complex CPSs.

## Key findings

- Proves energy safety and collision freedom for a ground rover system.
- Demonstrates system guarantees mission completion within time constraints.
- Introduces coordinated switching logic for nested and parallel Simplex instances.

## Abstract

We present Component-Based Simplex Architecture (CBSA), a new framework for assuring the runtime safety of component-based cyber-physical systems (CPSs). CBSA integrates Assume-Guarantee (A-G) reasoning with the core principles of the Simplex control architecture to allow component-based CPSs to run advanced, uncertified controllers while still providing runtime assurance that A-G contracts and global properties are satisfied. In CBSA, multiple Simplex instances, which can be composed in a nested, serial or parallel manner, coordinate to assure system-wide properties. Combining A-G reasoning and the Simplex architecture is a challenging problem that yields significant benefits. By utilizing A-G contracts, we are able to compositionally determine the switching logic for CBSAs, thereby alleviating the state explosion encountered by other approaches. Another benefit is that we can use A-G proof rules to decompose the proof of system-wide safety assurance into sub-proofs corresponding to the component-based structure of the system architecture. We also introduce the notion of coordinated switching between Simplex instances, a key component of our compositional approach to reasoning about CBSA switching logic. We illustrate our framework with a component-based control system for a ground rover. We formally prove that the CBSA for this system guarantees energy safety (the rover never runs out of power), and collision freedom (the rover never collides with a stationary obstacle). We also consider a CBSA for the rover that guarantees mission completion: all target destinations visited within a prescribed amount of time.