Formal design of embedded systems

4/16/2018

By Naijun Zhan, Distinguished Research Professor at the Chinese Academy of Sciences, China.

Abstract. I will report our on recent work on model-based formal design of embedded systems. In this approach, one can build a graphical model of a system to be developed with Simulink/Stateflow (S/S), and then conduct extensive simulation. In order to formally verify the graphical model, we translate S/S diagrams into HCSP automatically. HCSP is a formal modeling language for hybrid systems, which is an extension of CSP with differential equations intended to model continuous evolution and several kinds of interrupts capturing the interaction between continuous evolution and discrete jumps.

Using Hybrid Hoare Logic and its theorem prover, the translated HCSP formal model can be verified. In order to justify the correctness of the translation, we give an inverse translation from HCSP to Simulink, so that the consistency can be checked by co-simulation. Also, we define formal semantics of S/S and HCSP with UTP so that the correctness of the bidirectional translation can be proved theoretically. Finally, we propose a notion of approximate bisimulation for HCSP so that a given HCSP process can be correctly discretised. Based on this, we define a set of refinement rules to refine an HCSP process into a piece of SystemC code, proved to be approximate bisimilar to the original HCSP process. All the above are supported by a tool chain called MARS, whose application to real-world case studies will be mentioned.

Keywords. Software Engineering, Formal design, Embedded Systems.

About the Speaker. Naijun Zhan is a research professor of State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences. He got his bachelor and master degrees both from Nanjing University, and his PhD from the Institute of Software Chinese Academy of Sciences. Prior to join Institute of Software, Chinese Academy of Sciences, he worked at the Faculty of Mathematics and Informatics, Mannheim University, Germany as a research fellow.

He is a distinguished research professor at the Chinese Academy of Sciences (since 2015), and the winner of Outstanding Youth Fund of Natural Science Foundation of China (2016). His research interests cover formal design of real-time, embedded and hybrid systems, program verification, concurrent computation models, modal and temporal logics, and so on. Currently, he serves the editorial boards of Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Journal of Software, and Journal of Computer Research and Development.