Context
In cyber-physical systems (CPS), software interacts with physical processes so as achieve desired functionalities. 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. In addition, explainability of increasingly autonomous CPS is becoming crucial in order for the CPS to be socially acceptable. To formally reason about interactions between software (with discrete behavior) and physical processes (with continuous behavior), hybrid systems have become a commonly used mathematical model, since this formalism provides a clear definition and combination of continuous and discrete dynamics.
Objectives
The goal of this project is twofold. First, we will investigate a contract-based design approach for safe CPS in which different aspects – such as functional requirements, real-time constraints, and continuous behaviors – are modeled and verified separately. 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. This contract-based approach will thus enable complexity reduction by compositional reasoning. Such a reduction is crucial for scalability of hybrid systems analysis techniques used for the design of the components and their composition. Second, we will leverage the contracts in order to ensure explainability of the system behavior by construction. By explainability we understand, informally, that for any behavior of the system we can automatically construct, from a log generated by the execution, an excerpt that retains only the events that causally contributed to the outcome, and that is easy to understand by a human expert.
Application
Candidates should have a good background in formal methods. Good programming skills are a plus.
The PhD thesis will be co-advised by Gregor Goessler (SPADES team, INRIA Grenoble and LIG, firstname.lastname@inria.fr) and Thao Dang (VERIMAG, dangth@univ-grenoble-alpes.fr). Please do not hesitate to contact us for more information. To apply online please visit https://grenoble-inp.jobteaser.com/fr/job-offers/4851081-inria-grenoble-rhone-alpes-construction-of-safe-explainable-cyber-physical-systems
