Vous êtes ici

Refinement types for cyber-physical system design

Equipe et encadrants
Département / Equipe: 
Site Web Equipe: 
team.inria.fr/tea
Directeur de thèse
Jean-Pierre Talpin
Co-directeur(s), co-encadrant(s)
Contact(s)
Sujet de thèse
Descriptif

Tremendous accomplishments in the domains of type theory and formal verification over the past decade have led to the renovation and implementation of the "program has proof" paradigm using notions of refinement type.  A refinement type <x : t | p>  defines the data type t of values named x together with a property p that specifies properties of x within the domain of t and/or the context in which that value is defined.  “clean slate” programming languages such as Liquid Haskell, F*, and many others, implement specification and proof of refinement types using SAT-SMT verification (Z3) and proof engines (Coq).

Objective
We wish to cast the concept of refinement type to the context of an end-to-end design methodology for cyber-physical systems.  To this end, we wish to propose an algebraic framework on which to reason about the composition, abstraction, refinement, of individual, heterogeneous, CPS components by means of interface or contract algebras expressing first and higher order logic properties about assumptions and guarantees of system's constituants to be assembled.


Profil
We are looking for a talented candidate with demonstrated knowledge and experience in type theory, contracts theory, formal verification, concurrency theory and control. This PhD proposal is in the frame of Inria's associate team Composite with UC San Diego MESL and project-team TEA.

 

Bibliographie

1. "Programming with Refinement Types: An Introduction to LiquidHaskelll". R. Jhala, E. Seidel, N. Vazou. UCSD, 2017. https://ucsd-progsys.github.io/liquidhaskell-tutorial

2. "Verified programming in F*". The F* team, MSR-Inria , 2017. https://www.fstar-lang.org/tutorial

3. "Differential dynamic logic dL". A. Platzer, Logical analysis of hybrid systems. Springer, 2010.

4. "Compositional proofs in dynamic differential logic". S. Lunel, B. Boyer, J.-P. Talpin. Submitted to Application of concurrency to system design (ACSD'17).  IEEE, 2017.

5. "Cyber-Physical System Design from an Architecture Analysis Viewpoint". S. Nakajima, Talpin, J.-P., M. Toyoshima, H. Yu, Editors. Communications of the NII Shonan Meetings, Springer, 2017.

Début des travaux: 
Automne 2017
Mots clés: 
type theory, concurrency, contract theories, system design, cyber-physical systems
Lieu: 
IRISA - Campus universitaire de Beaulieu, Rennes