2019-01424 - PhD Position F/M "A logical framework to verify requirements of hybrid system models"
Le descriptif de l’offre ci-dessous est en Anglais

Niveau de diplôme exigé : Bac + 5 ou équivalent

Fonction : Doctorant

Contexte et atouts du poste

Context

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).

 

Mission confiée

As a result, two artifacts should be investigated and developed:

  1. 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.
  2. 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 [8]. 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.

Principales activités

Objectives

The first part of the doctoral project will build upon previous works combining the use of logical models of CPSs [1] and contract-based design [2]. In [4], 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 [5], 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 [9].

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 [4] 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 [3].

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.

References

[1] Logical foundations of cyber-physical systems. André Platzer. Springer, 2018. ISBN 978-3-319-63588-0.

[2] Contracts for system design A. Benveniste et al. RR-8147, INRIA. 2012. hal-00757488

[3] “Handbook of Hybrid Systems Control: Theory, Tools, Applications.” J. Lunze, F. Lamnabhi-Lagarrigue, Cambridge University Press.

[4] "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.

[5] “Mixing proved and unproved system parts through contracts to ensure correct-by-construction system design”.  Antonin Butant, Master internship report, 2016.

[6] 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.

https://doi.org/10.1145/3019612.3019787

[7] 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

[8] 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.

[9] 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.

 

Compétences

Applications

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). 

 

Avantages

  • Subsidized meals
  • Professional equipment available (videoconferencing, loan of computer equipment, etc.)
  • Social, cultural and sports events and activities
  • Access to vocational training