多异质嵌入式系统的建模、仿真与验证研究
结题报告
批准号:
61972385
项目类别:
面上项目
资助金额:
60.0 万元
负责人:
王淑灵
学科分类:
计算机科学的基础理论
结题年份:
2023
批准年份:
2019
项目状态:
已结题
项目参与者:
王淑灵
国基评审专家1V1指导 中标率高出同行96.8%
结合最新热点,提供专业选题建议
深度指导申报书撰写,确保创新可行
指导项目中标800+,快速提高中标率
客服二维码
微信扫码咨询
中文摘要
随着新的计算、控制等技术的发展,嵌入式系统被越来越广泛地应用于安全攸关领域中。如何保障安全攸关嵌入式系统的正确性,是学术界和工业界亟待解决的难题。然而,现代嵌入式系统设计是一个复杂的工程,既涉及系统体系结构、协同设计等系统级问题,又涵盖离散与连续数据流、各种控制逻辑等功能行为。从这些问题出发,本项目将建立同时包含系统体系结构和功能行为的多异质嵌入式系统的建模、仿真与验证框架。考虑到工程应用角度和高可靠需求,我们将建立嵌入式系统的图形化集成建模语言,该语言具有明确的语义,并支持对模型的协同仿真分析;同时,我们将定义嵌入式系统的形式化建模语言,支持对模型的形式化验证,严格保证系统的正确性。我们还将实现从图形模型到形式模型的自动转换,并严格证明转换的一致性。以上语义定义和证明均在Isabelle中形式化,对可靠性提供很高的保障。本项目所产生的方法和工具,将应用到航天、汽车等领域选取的具体案例中。
英文摘要
With the development of new techniques in computing and control, embedded systems are applied more and more in safety-critical areas. How to guarantee the correctness of an embedded system, is a challenge faced by both the academia and the industry community. However, the design of embedded systems is a complicated engineering process. It needs to consider the system-level design issues such as system architecture and co-design, and at the same time, it must also realize different functional behaviors such as discrete and continuous dataflows and complex control flows. To address these issues, this project aims to develop a framework for the modelling, simulation and verification of heterogeneous embedded systems, by considering both architecture and functionality. Considering the requirements from both practical engineering and high safety, we will build an integrated graphical modelling language, with precise semantics and supporting simulation analysis to models; meanwhile, we will also define a formal modelling language for embedded systems, and perform formal verification to the formal models to guarantee the correctness. We will implement the automatic model transformation from graphical models to formal models, and moreover, prove the correctness of the transformation in a rigorous way. All the semantics and proofs in this project are formalized in Isabelle, thus provide a high guarantee for reliability. We will apply the methods and tools developed in the project to the real case studies chosen from the aerospace and automotive industry.
期刊论文列表
专著列表
科研奖励列表
会议论文列表
专利列表
DOI:10.1145/3631483.3631487
发表时间:2023-10
期刊:ACM SIGAda Ada Letters
影响因子:--
作者:Xiong Xu;Shuling Wang;Bohua Zhan;Xiangyu Jin;N. Zhan;J. Talpin
通讯作者:Xiong Xu;Shuling Wang;Bohua Zhan;Xiangyu Jin;N. Zhan;J. Talpin
DOI:10.1007/s11390-020-0537-8
发表时间:2020
期刊:JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY
影响因子:1.9
作者:Lin Qianqian;Wang Shuling;Zhan Bohua;Gu Bin
通讯作者:Gu Bin
DOI:10.1007/s11432-020-3266-6
发表时间:2023-01
期刊:Science China Information Sciences
影响因子:--
作者:Wenyou Liu;Yunjun Bai;Li Jiao;N. Zhan
通讯作者:Wenyou Liu;Yunjun Bai;Li Jiao;N. Zhan
Safe Reinforcement Learning Algorithm and Its Application in Intelligent Control for CPS
安全强化学习算法及其在CPS智能控制中的应用
DOI:10.21655/ijsi.1673-7288.00284
发表时间:2022
期刊:International Journal of Software and Informatics
影响因子:--
作者:Hengjun Zhao;Quanzhong Li;Xia Zeng;Zhiming Liu
通讯作者:Zhiming Liu
DOI:10.1016/j.sysarc.2022.102665
发表时间:2022
期刊:Journal of Systems Architecture
影响因子:--
作者:Panhua Guo;Bohua Zhan;Xiong Xu;Shuling Wang;Wenhui Sun
通讯作者:Wenhui Sun
面向对象程序的形式化规范与验证
  • 批准号:
    61100061
  • 项目类别:
    青年科学基金项目
  • 资助金额:
    24.0万元
  • 批准年份:
    2011
  • 负责人:
    王淑灵
  • 依托单位:
国内基金
海外基金