王淑灵-复杂安全攸关嵌入式系统的形式设计与实现V3.pdf

《王淑灵-复杂安全攸关嵌入式系统的形式设计与实现V3.pdf》由会员分享，可在线阅读，更多相关《王淑灵-复杂安全攸关嵌入式系统的形式设计与实现V3.pdf（30页珍藏版）》请在三个皮匠报告上搜索。

1、复杂安全攸关嵌入式系统的形式设计与实现王淑灵 中国科学院软件研究所目 录CONTENTS1.背景和问题2.基于Simulink/Stateflow和AADL的协同设计3.HCSP形式建模和验证4.已验证模型到代码的生成5.应用背景和问题PART 01研究背景安全攸关嵌入式系统是国民经济的重要基础和国家重大任务的核心支撑。安全攸关嵌入式控制系统广泛应用于国防、交通、高端制造等关键领域，其失效可能导致人员重大伤亡、财产重大损失、环境重大破坏等灾难性后果。2018年狮航波音737 Max空难2011年“甬温”列车相撞事故近年，安全攸关嵌入式控制系统缺陷导致的重大事故频发，其可信性设计亟待突破安全攸关

2、嵌入式系统的设计如何设计安全可靠的嵌入式系统是计算机科学和控制理论的一个巨大挑战“the challenge of designing embedded systems offers a unique opportunity for reinvigorating computer science.The challenge,and thus the opportunity,spans the spectrum from theoretical foundations to engineering practice.To begin with,we need a mathematical bas

3、is for systems modeling and analysis which integrates both computation and physical constraints in a consistent,operative manner.”“The Embedded Systems Design Challenge”Invited talk at FM 2006Joseph Sifakis2007年图灵奖获得者法兰西科学院荣誉研究主任Tom HenzingerAAAS、ACM、IEEE Fellow欧洲科学院、德国科学院、奥地利科学院院士奥地利科学院院长形式建模、分析与验证

4、是安全攸关嵌入式系统可信保障的核心技术，已经成为各种行业和国际标准的共识基于模型的嵌入式系统形式设计（MBD）主要挑战：复杂性 可靠性MBD的复杂结构 横向：组合/分解 纵向：抽象/精化MBD的设计方法 基于图形建模与仿真的设计易使用（工程师）高效，但不完备 基于形式建模与验证的设计可靠，难掌握（理论专家）、代价高我们的方法MARS：Modelling,Analysis and verification of Hybrid Systems研究团队：周巢尘，詹乃军，王淑灵，詹博华，徐雄等基于Simulink/Stateflow和AADL的协同设计PART 02AADL+Simulink/Stat

5、eflow 图形化协同设计 嵌入式系统设计Functionality(F)：软件行为Physicality(P)：物理环境 Architecture(A)：体系结构和硬件平台 AADL(F-,P-,A+)基于模型驱动的系统架构设计语言，被广泛应用于航空航天等工程设计领域。Simulink/Stateflow(F+,P+,A-)工业界开发嵌入式系统的实际标准。建模嵌入式系统中复杂的离散和连续行为，支持高效仿真和代码生成。AADL+Simulink/Stateflow协同建模和仿真将嵌入式系统的软件、硬件以及物理环境在一个统一的框架下进行建模和仿真。如何将Simulink/Stateflow模型与

6、AADL模型进行集成？将S/S模型定义为AADL的抽象类型，声明输入/输出端口。定义AADL和S/S之间的端口对应关系，进行数据之间的传输。如何进行协同仿真？实现 AADL2C转换器，将AADL模型转换为C代码进行功能和性能的仿真。应用Matlab的实时工具箱RTW，将S/S模型自动生成C代码。将分布式构件之间对应的端口进行连接，进行系统级别的仿真。HCSP形式建模和验证PART 03混成通信顺序进程（HCSP）HCSP，在通信顺序进程（Hoare，CSP）的基础上，引入用于描述连续行为的微分方程，以及用于描述连续行为和离散行为交互的中断机制。其中，ch