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.

Paritcipants


  • Thierry Gautier and Jean-Pierre Talpin, Inria project-team TEA
  • Naijun Zhan, Institute of Software, Chinese Academy of Science
  • Kai Hu, Beijing University of Aeronautics and Astronautics (Beihang)
  • Zhang Yushi, Coputer Science Department, Nankai University
  • Zhibin Yang, Nanjing University of Aeronautics and Astronautics (Nanhang)
  • Jifeng He and Yongxin Zhao, East-China Normal University
  • Ding Yi, School of Information, Beijing Wuzi University

Publications

Events