Context
Cyber-Physical Systems 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.
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 exact methods; often one has to use approximations. Existing methods and tools for formal analysis of hybrid systems do not scale well and only allow, in practice, for partial analysis of systems due to their high complexity.
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. We also consider the problem of generating contracts from experimental data of practical systems.
The goal of this thesis is to develop a contract-based design approach for hybrid systems, in order to overcome the current limitations of formal analysis.
Working Context The thesis will be co-advised by Thao Dang (Verimag) and Gregor Goessler (INRIA). The PhD student will be hosted by the Verimag laboratory, near Grenoble in the French Alps.
Required Skills Candidates should have good background in formal methods. and continuous mathematics. Good programming skills are also required.
Application Interested candidates should send a cover letter and CV to Thao Dang Firstname.Lastname@imag.fr. and Gregor Goessler INRIA Grenoble - Rhône-Alpes, SPADES team Firstname.Lastname@inria.fr
