Level of qualifications required : Graduate degree or equivalent
Fonction : PhD Position
The goal of this doctoral project is to verify and build cyber-physical systems (CPSs) with a correct-by-construction approach in order to validate system requirements against models of the cyber and physical elements of such designs. Our approach is based on components augmented with formal contracts that can be composed, abstracted or refined. It fosters the proof of system-level requirements by composing individual properties proved at component level. While semantically grounded, the tooling of this methodology should be usable by regular engineers (i.e. not proof theory specialists).
As a result, two artifacts should be investigated and developed:
- A logical framework providing the theoretical foundation on which the semantics of the components and their interactions can be expressed and used for proving key properties. This logical framework should be accompanied by a methodology prescribing how to use the framework to effectively build CPSs, i.e. model the continuous part and specify and implement the discrete part, in order to ultimately verify key properties against the behavior obtained by composition.
- A user-level approach to describe formal specifications that is expressive, user friendly and can be translated into the above logical framework. In particular, a Simulink-like approach (dataflow oriented language) will be considered to specify the both continuous and discrete parts of CPSs . This language will also be able to express contracts and invariants about the system’s components in order to specify the typical systems requirements (functional, latency, timing, energy…) of CPSs.
The first part of the doctoral project will build upon previous works combining the use of logical models of CPSs  and contract-based design . In , we proposed a method to formalize CPS components using dynamic differential logic together with a composition theorem automating the proof of system properties from mechanized proofs of elementary system components. In , we designed a component based approach for system design exploiting the capabilities of this framework with an executable semantics of contracts. These notions will be furthered with the introduction of communication and concurrency that proved to facilitate composition in related frameworks, such as HCSP .
The goal will hence be to merge the above concepts into a coherent framework and apply it to specify the semantics of data-flow, Simulink-like, component specifications allowing to equally model and prove continuous and discrete artifacts. The logical framework will allow to verify system requirements seen as properties implied by the differential invariants of the analog model at the interface between the cyber and physical worlds (i.e., the system architecture).
The contracts of such components will consist of guarded actions and/or (quantitative) logical propositions in Hoare logic. The method we developed in  tackles the scalability issues for verifying such properties on an entire system by splitting the verification problem into the (possibly mechanized) verification of local properties such as contracts or invariants attached to system components. Still, in order to fully automate verification, another objective of the project will be to organize existing proof tools (SMT-solvers, model-checkers, ODE-solvers…) in such a way that industrially relevant properties can indeed be proved, e.g., verify requirements against refinements of digital and analog components. Integrating these tools should facilitate and maximize proof automation. In case of errors, counter-examples should be ultimately reported at user-level, i.e. at the same description level that the initial requirements and specifications developed in the second part.
The second part of the project will be to capture and formalize user requirements and specifications to support their formal verification in an industrial workflow of CPS design. The considered CPS models are implemented in a dataflow oriented language (Simulink-like) augmented with contracts and invariants expressed in a user-friendly form. The envisioned environment shall be usable to model discrete and continuous parts of the system as well as its properties and requirements. The specification language shall in particular express templates for typical properties sought in control theory .
In order to concretely guide and evaluate the development of the overall approach, Mitsubishi Electric R&D Centre Europe will provide a set of industrially relevant use cases from railway, automotive or factory automation domains.
 Logical foundations of cyber-physical systems. André Platzer. Springer, 2018. ISBN 978-3-319-63588-0.
 Contracts for system design A. Benveniste et al. RR-8147, INRIA. 2012. hal-00757488
 “Handbook of Hybrid Systems Control: Theory, Tools, Applications.” J. Lunze, F. Lamnabhi-Lagarrigue, Cambridge University Press.
 "Compositional proofs in dynamic differential logic". S. Lunel, B. Boyer, J.-P. Talpin. International Conference on Applications of Concurrency to System Design (ACSD'17). Springer, 2017.
 “Mixing proved and unproved system parts through contracts to ensure correct-by-construction system design”. Antonin Butant, Master internship report, 2016.
 Predrag Filipovikj, Guillermo Rodriguez-Navas, Mattias Nyberg, and Cristina Seceleanu. 2017. SMT-based consistency analysis of industrial systems requirements. In Proceedings of the Symposium on Applied Computing (SAC '17). ACM, New York, NY, USA, 1272-1279.
 Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, and André Platzer. 2018. VeriPhy: verified controller executables from verified cyber-physical system models. SIGPLAN Not. 53, 4 (June 2018), 617-630. https://doi.org/10.1145/3296979.319240
 Mengfei Yang and Naijun Zhan: Combining Formal and Informal Methods in the Design of Spacecrafts. In SETSS 2014, Lecture Notes in Computer Science 9506, Springer-Verlag. 2016.
 Naijun Zhan, Shuling Wang and Hengjun Zhao: Formal Modelling, Analysis and Verification of Hybrid Systems. In the Theories of Programming, Lecture Notes in Computer Science 8050, Springer-Verlag. 2013.
The ideal candidate will have a strong background in mathematical logic, concurrency theory, formal verification, and experience and interest in program analysis, control theory and embedded system design. Depending on background and experience, the candidate will engage in either or both of the challenges posed by the verification of digital and analog requirements.
The successful applicant will be employed by Mitsubishi Electric R&D Centre Europe under a CIFRE grant (3 years contract) and embedded with Inria project-team TEA at Inria, Rennes (Brittany, France).
- Subsidized meals
- Professional equipment available (videoconferencing, loan of computer equipment, etc.)
- Social, cultural and sports events and activities
- Access to vocational training
- Theme/Domain : Proofs and Verification
- Town/city : Rennes
- Inria Center : CRI Rennes - Bretagne Atlantique
- Starting date : 2019-10-01
- Duration of contract : 3 years
- Deadline to apply : 2019-06-30
Inria, the French national research institute for the digital sciences, promotes scientific excellence and technology transfer to maximise its impact. It employs 2,400 people. Its 200 agile project teams, generally with academic partners, involve more than 3,000 scientists in meeting the challenges of computer science and mathematics, often at the interface of other disciplines. Inria works with many companies and has assisted in the creation of over 160 startups. It strives to meet the challenges of the digital transformation of science, society and the economy.
Instruction to apply
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.