Research

CONVEX:Compositional Verification of Cyber-Physical Systems (2018 Associate Team’s Call)

2018 / 07 / 26

Inria

Research center: CRI Rennes - Bretagne Atlantique

Inria Research team : TEA

Principal investigator : Thierry Gautier

Field : Algorithmics, Programming, Software and Architecture

Theme : Embedded and Real-time Systems


International Partners

- Naijun Zhan, State Key Laboratory of Computer Science of the Chinese Academy of Sciences

- Kai Hu, Beijing University of Aeronautics and Astronautics

- Zhibin Yang, Nanjing University of Aeronautics and Astronautics

- Yushi Zhang, Computer Science Department of Nankai University

Creation: February 2018


Project Description 

Formal modeling and verification methods have successfully improved software safety and security in vast application domains in transportation, production and energy. However, formal methods are labor-intensive and require highly trained software developers. Challenges facing formal methods stem from rapid evolution of hardware platforms, the increasing amount and cost of software infrastructures, and from the interaction between software, hardware and physics in networked cyber-physical systems. Automation and expressivity of formal verification tools must be improved not only to scale functional verification to very large software stacks, but also verify non-functional properties from models of hardware (time, energy) and physics (domain). Abstraction, compositionality and refinement are essential properties to provide the necessary scalability to tackle the complexity of system design with methods able to scale heterogeneous, concurrent, networked, timed, discrete and continuous models of cyber-physical systems. Project CONVEX wants to define a CPS architecture design methodology that takes advantage of existing time and concurrency modeling standards (MARTE, AADL, Ptolemy, Matlab), yet focuses on interfacing heterogeneous and exogenous models using simple, mathematically-defined structures, to achieve the single goal of correctly integrating CPS components.


For more information on this scientific project, please visit the dedicated website:  http://www.irisa.fr/prive/talpin/convex/

+86 (0) 10 8254 4772

+86 (0) 10 8254 4594

xuefei.liu@nlpr.ia.ac.cn

5F, Intelligent Building N.95, Zhong Guan Cun East Road, Beijing, China