EVENT

Event News

ERATO Project Colloquium by Naijun Zhan

On Tuesday 4 February, Naijun Zhan (Peking University) will give a talk, "Formal Design of Safety-critical Embedded Systems", for our project colloquium at 16:30. Further details can be found below.

Title:

Formal Design of Safety-critical Embedded Systems

Speaker:

Naijun Zhan (Peking University)

Abstract:

I will report our recent work on model-based formal design of safety-critical embedded systems. With our approach, one can build a graphical model for a system to be developed with the combination of Simulink/Stateflow and AADL (AADL+S/S), and then conduct extensive simulation. An AADL+S/S graphical model can be translated to an HCSP formal model automatically, so that the translated HCSP formal model can be verified using Hybrid Hoare Logic with its theorem prover. To justify the correctness of the translation, we define formal semantics of AADL+S/S and HCSP respectively with HUTP (Higher-order Unifying Theories of Programming). Finally, we propose the notion of approximate bisimulation for HCSP, and 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 applied the above approach to design some real-world case studies.

Biography:

Naijun Zhan is a Boya distinguished professor in the School of Computer Science of Peking University. He got his bachelor degree and master degree both from Nanjing University, and his PhD from Institute of Software Chinese Academy of Sciences (ISCAS). Prior to join Peking University, he worked at the Faculty of Mathematics and Informatics, Mannheim University, Germany as a research fellow, and afterwards worked at ISCAS as an associate professor, a full professor, and a distinguished professor. His research interests cover formal design of real-time, embedded and hybrid systems, program verification, and so on. He is in the editorial boards of Journal of Automated Reasoning, 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 and so on, a member of the steering committees of SETTA and MEMOCODE, the pc co-chairs of FM 2021, SETTA 2016, the general co-chairs of MEMOCODE2018, 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 150 papers in international leading journals and conferences and 2 books, and edited 4 conference proceedings and 7 journal special issues. See lcs.ios.ac.cn/~znj for more details.

Time/Date:

16:30- / Tuesday 4 February , 2025

Place:

NII Room 1310A and Online

Link:

For the latest information about ERATO colloquium/seminar, please see the webpage.
https://docs.google.com/document/d/1Qrg4c8XDkbO3tmns6tQwxn5lGHOrBON5LtHXXTpXDeA/edit

Contact:

Kittiphon Phalakarn (ERATO MMSD Colloquium Organizer)
Email: kphalakarn[at] nii.ac.jp

entry6750

SPECIAL