Quantitative Safety-Driven Co-Synthesis of Cyber-Physical System Implementations

Feedback controllers form the algorithmic core of many cyber-physical systems (CPSs). They are increasingly becoming computationally expensive and efficiently implementing them on resource-constrained platforms—such as those in the automotive domain—while guaranteeing safety is now an important challenge. Current workflows allow control strategies to be designed independently of the implementation environment and require control tasks to meet predetermined deadlines. Embedded systems engineers treat these control tasks as black boxes and focus on meeting all deadlines as the mechanism for ensuring safety. In this paper, we argue that deadlines are only a means to an end and should not be treated as "first-class citizens." Instead, the focus should be on high-level safety properties of relevance. Our main technical contribution is in automatic synthesis of safe CPS implementations: given a set of controllers to be implemented on a shared resource, along with their safety properties (a form of state space trajectory robustness), we synthesize an implementation that does not necessarily meet all task deadlines, but guarantees the safety specifications of all controllers.