Rigorous Design of Cyber-physical Systems

Cyber-physical systems (CPS) break with traditional systems such as desktop computers and servers, in various ways: (1) they are instrumented in order to interact with physical environments; (2) they are interconnected to allow interaction between people and objects in entirely new modes; (3) they must be smart to ensure predictability of events and optimal use of resources. Currently, we lack theory methods and tools for building cost-effectively trustworthy CPS. In this talk, I will show how and why CPS challenge our capabilities for ensuring their trustworthiness. I will advocate for a coherent scientific foundation of CPS design and will discuss three main scientific challenges: (1) Marrying physicality and computation; (2) Correctness-by-construction; (3) Adaptivity. Meeting these challenges is a prerequisite for moving from empirical to rigorous design. This can be formalized as a sound, scalable and accountable process leading to trustworthy and optimized implementations from: (1) an application software; (2) models of its execution infrastructure; and (3) models of its physical environment. Soundness is achieved through translation of the languages used along the design process into a single and expressive host language rooted in clean operational semantics. Scalability and accountability can be ensured by using correct-by-construction source-to-source transformations in the host language. The talk will conclude with an overview of the BIP rigorous design flow developed at Verimag and EPFL.