计算机学科前沿论坛之十九
报告题目：Formal design of safety-critical embedded systems
报告人：詹乃军 中国科学院软件研究所特聘教授、博士生导师、国家杰出青年科学基金获得者
报告时间：2022年11月16日下午2:30-3:30
腾讯会议：348-455-212
报告摘要: I will report our recent work on model-based formal design of embedded systems. In our approach, one can build a graphical model of a system to be developed with the combination of AADL and Simulink/Stateflow, called AADL+S/S, and then conduct extensive simulation. In order to formally verify the graphical model, we translate AADL+S/S models into HCSP automatically. HCSP is a formal modeling language for hybrid systems, which is 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 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 AADL+S/S and HCSP with UTP so that the correctness of the bidirection translation can be proved theoretically. Finally, we propose the notion of approximate bisimulation for HCSP so that we can discretise a given HCSP process correctly in the sense of approximate bisimulation. Based on which, we define a set of refinement rules through which we can refine an HCSP process into a piece of SystemC or ANSI-C code, which is approximate bisimilar to the original HCSP process. All the above are supported by a tool chain called MARS. We have applied the above approach to design some real-world case studies.
报告人简介：
Naijun Zhan is a distinguished research professor of Institute of Software Chinese Academy of Sciences (ISCAS). He got his bachelor degree and master degree both from Nanjing University, and his PhD from ISCAS. Prior to join ISCAS, he worked at the Faculty of Mathematics and Informatics, Mannheim University, Germany as a research fellow. 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. He is in the editorial boards of Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Journal of Software, Journal of Electronics, and Journal of Computer Research and Development, a member of the steering committees of SETTA and MEMOCODE, the pc co-chairs of FM 2021, SETTA 2016, the general co-chairs of MEMOCODE 2018, MEMOCODE2019 and ICESS 2019, and serves more than 100 international conferences program committees e.g., CAV, RTSS, HSCC, FM, TACAS, EMSOFT and so on. He published more than 100 papers in international leading journals and conferences, 2 books and 4 book chapters, and edited 4 conference proceedings and 5 journal special issues. See lcs.ios.ac.cn/~znj for more details.
