Cyber-physical systems (CPS) are software-controlled physical systems, that arise in many application domains, ranging from automotive to aerospace to process control. The design challenges associated with CPS include ensuring the required functional properties, assessing safety aspects with appropriate management of faults, and the exploration of the space of possible solutions.
In this lecture, we overview the application of novel formal verification to such challenges. Within a formal contract-based framework we cover the problems of hierarchical decomposition, requirements analysis, fault tree generation, and synthesis of optimal configurations.
At the core of the approach, CPS are represented by means of hybrid automata, taking into account the continuous evolution of the state over time. We adopt a symbolic representations that can be analyzed by means of model checking based on Satisfiability modulo Theories.