Shuling Wang, SKLCS, Institute of Software, Chinese Academy of Sciences
Formal Design of Cyber-Physical Systems


Cyber-physical systems (CPS) make use of computer units to control physical processes so that the behavior of the controlled processes meets expected requirements. They have become ubiquitous in our daily life, e.g., automotive, aerospace, medical systems and so on. The development of CPS is highly complex and challenging. Model-Based Design (MBD) is considered as an effective way of developing complex CPSs, and especially, to improve the efficiency and reliability, the automation of the whole system-design process of MBD is absolutely necessary.
In this tutorial, we will introduce the formal design of CPS based on the MBD approach, including the modelling, verification, and code generation. At the beginning, we start from building executable models of CPS using the industrial standard Simulink/Stateflow, which facilitates analysis by simulation. We will then present an encoding of the precise semantics in terms of HCSP, a formal modelling language for hybrid systems by extending CSP, thus provide an automatic translation from Simulink/Stateflow to HCSP formal models. The HCSP models can be formally verified in our theorem prover. After the HCSP models are proved correct, we will present how to generate SystemC code (only with discrete behavior) from the HCSP models (with both continuous and discrete behavior). To guarantee the correctness of the final code, we have proved the consistency between the source and target models for both the above model transformation.