2019-01540 - Post-Doctoral Research Visit F/M Compositional verification and synthesis from hybrid specifications
Le descriptif de l’offre ci-dessous est en Anglais

Niveau de diplôme exigé : Thèse ou équivalent

Fonction : Post-Doctorant

Niveau d'expérience souhaité : Jeune diplômé

A propos du centre ou de la direction fonctionnelle

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.

Contexte et atouts du poste

Recent advances in proof theory and formal verifications have brought logical frameworks enabling the verification and proof of hybrid system models: the solvers dReal and dReach [6], the prover Keymaera [7], and the Isabelle framework of HCSP [3,4,5].  These tools allow to interface the otherwise heterogeneous software, hardware and physical elements of a hybrid system in a unifying logical manner. Recent advances demonstrated that such interfaces could support modular, compositional, design and proof methodology [1,2].

In the context of Inria associate-team CONVEX, the goal of our post-doctoral project is to develop and tool a compositional methodology to verify and build cyber-physical systems (CPSs) by the modular assembly and iterative proof of their digital and analogic components.   

Mission confiée

The goal of our post-doctoral project is to develop and tool a compositional methodology to verify and build cyber-physical systems (CPSs) by the modular assembly and iterative proof of their digital and analogic components.   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 aims at being usable by regular engineers (i.e. not proof theory specialists). 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.
  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, an approach mixing AADL-like and Simulink-like dataflow diagrams will be considered to specify the both continuous and discrete components of CPSs [8].

Principales activités

References

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

[2] “Parallel Composition of Periodic Components in Differential Dynamic Logic”. Simon Lunel, Stefan Mitsch, Benoît Boyer and Jean-Pierre Talpin. Submitted for publication, 2019.

[3] Dimitar P. Guelev, Shuling Wang, Naijun Zhan (2017): Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus. In Proc. of SETTA2017, Lecture Notes in Computer Science 10606, pp.110-127.

[4] Gaogao Yan, Li Jiao, Shuling Wang and Naijun Zhan (2017): Generating SystemC code from delay HCSP. In Proc. of APLAS 2017, Lecture Notes in Computer Science 10695, pp.21-41.

[5] Ehsan Ahmad, Brian Larson, Stephen Barrett, Naijun Zhan and Yunwei Dong (2014): An AADL Extension for Continuous Behavior and Cyber-Physical Interaction Modeling, in Proc. of HILT 2014, pp.29-38.

[6] dReal: An SMT Solver for Nonlinear Theories over the Reals. Sicun Gao, Soonho Kong, Edmund M. Clarke.  Lecture Notes in Computer Science, volume 7898 (CADE’13). Springer, 2013.

[7] André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, Cham, 2018. 659 pages. ISBN 978-3-319-63587-3.

 

Avantages

  • Subsidized meals
  • Partial reimbursement of public transport costs
  • Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours)
  • Professional equipment available (videoconferencing, loan of computer equipment, etc.)
  • Social, cultural and sports events and activities
  • Access to vocational training
  • Social security coverage

Rémunération

Monthly gross salary amounting to 2653 euros.