Formal design of embedded real-time systems

Abstract

Recently we propose an approach to designing embedded real-time systems formally. Using our approach, one can first build a graphical model of a system to be developed with Simulink/Stateflow (S/S), and then conduct extensive simulation. In order to verify the graphical model formally, we translate S/S diagrams into HCSP automatically. HCSP is a formal modeling language for hybrid systems, an extension of CSP by introducing differential equations to model continuous evolution and several kinds of interrupts to model the interaction between continuous evolution and discrete jumps. Using Hybrid Hoare Logic and its theorem prover, the translated HCSP model can be verified. For justifying the correctness of the translation, we give an inverse translation from HCSP to Simulink, so that the consistency can be checked by co-simulation. By providing a set of refinement rules, an HCSP process can be generated into a piece of SystemC code, approximate bisimilar to the original HCSP process. All work can be supported by a developed tool MARS. Several real-world case studies have been investigated to check the feasibility of the approach.

Biography

Prof. Naijun Zhan is a distinguished research professor of State Key Lab. of Computer Science, Institute of Software, the Chinese Academy of Sciences. He got his bachelor degree and master degree both from Nanjing University, and his PhD from 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 the winner of Outstanding Youth Fund of Natural Science Foundation of China of 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. Now, he serves the editorial boards of Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Journal of Software, Journal of Computer Research and Development.