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

Updated: 2018/7/26   
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:
回首页 回前页 回到页首