• 首页
  • 学院概况
    学院简介 现任领导 组织机构 学科概况
  • 师资队伍
    学院教师
  • 人才培养
    本科生教育 研究生教育 基层教学组织
  • 科学研究
    学术交流 科研平台
  • 党群工作
    党群动态 规章制度 学院工会 关工委 妇委会
  • 学生工作
    组织架构 学工动态 规章制度 青春榜样
  • 校友工作
    校友动态 校友风采
首页
  • 新闻动态
  • 通知公告
  • 学术交流
  • 学生活动
  • 师生风采
  • 教学科研
学术交流
首页 > 学术交流 > 正文

计算机学科前沿论坛之十九——Formal design of safety-critical embedded systems

日期:2022-11-14 责任编辑:沙艳 浏览量:
地点: 腾讯会议:348-455-212 报告人: 詹乃军
日期: 2022.11.16

计算机学科前沿论坛之十九

报告题目: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.




  • 附件【计算机学科前沿论坛19.docx】已下载次

上一篇:计算机学科前沿论坛之二十——基于图差异移植的软件自动修复技术 下一篇:计算机学科前沿论坛之十八——智能数据库系统研究:技术与挑战
大学计算机
基础课程预约
专业认证资料
管理系统
全国计算机等级
考试报名
基础试验网
专业资源网
会议室、实验室
使用预约
报修预约

邮编:221116 联系电话:0516-83591709

地址:江苏省徐州市大学路1号中国矿业大学南湖校区

版权所有:中国矿业大学计算机科学与技术学院/人工智能学院

官方微博
微信公众号