Franz Franchetti, Tze-Meng Low, Stefan Mitsch, Juan Pablo Mendoza, Liangyan Gui, Amarin Phaosawasdi, David Padua, Soummya Kar, Josť M. F. Moura, M. Franusich, Jeremy Johnson, Andre' Platzer and Manuela Veloso (IEEE Control Systems Magazine, 2017)
High-Assurance SPIRAL: End-to-End Guarantees for Robot and Car Control
Preprint (4.4 MB)
Published paper (link to publisher)

Cyber-physical systems (CPSs), ranging from critical infrastructures such as power plants, to modern (semi) autonomous vehicles, are systems that use software to control physical processes. CPSs are made up of many different computational components. Each component runs its own piece of software that implements its control algorithms, based on its model of the environment. Every component then interacts with other components through the signals and values it sends out. Collectively, these components, and the code they run, drive the complex behaviors modern society has come to expect and rely on. Due to these intricate interactions between components, managing the hundreds to millions of lines of software to ensure that the system, as a whole, performs as desired can often be unwieldy.

SPIRAL, High assurance, Control systems