Fully Funded PhD Thesis: Safe Contract-Based Design of Cyber-Physical Systems (with scholarship from AGIR Grenoble Innovation Recherche)

Anti-lock breaking systems, temperature regulation in buildings, and drug infusion pumps are examples of cyber-physical systems (CPS) where software interacts with physical processes so as to ensure a desired safe and efficient behavior. CPS are usually subject to safety and reliability requirements. Depending on the application, their failure may have unacceptable consequences. It is therefore crucial to ensure their correctness at design time. Goals This thesis focuses on contract-based design of safe CPS. The contract of a component formally specifies the hypotheses the component makes on its environment, and its commitments (or expected behavior) in case the hypotheses are verified. In order to reason about interactions between software and physical processes one has to use hybrid models combining continuous and discrete dynamics. In addition to the problem of undecidability, several characteristics of hybrid systems such as their infinite state space and the lack of analytic solutions for systems described by differential equations, make these systems particularly hard to analyze using exac