随着功能需求的不断增加,安全关键系统的设计变得越来越复杂。如何通过建模与验证的方法保证安全关键系统的质量,一直以来都是形式化方法领域备受关注的问题。AADL作为一种应用广泛的建模语言,在安全关键系统的设计与实现中发挥着重要的作用。它提供了丰富的组件用来描述系统的体系结构,并且能够支持性能关键属性的早期预测和重复性分析。然而,AADL描述系统行为的方式主要是基于自动机理论,在建模和验证大型复杂系统时难免会遇到状态空间爆炸问题。此外,由于缺乏描述行为细节的手段,AADL难以支持功能需求的分析与验证,从而无法保证整个系统的正确性和安全性。针对AADL语言在行为描述以及模型验证上的不足,本文提出了一种基于约束求解的精化行为建模方法。该方法扩展了AADL语言以增强其描述行为细节的能力,并且能够支持Z3求解器对构建的精化行为模型进行分析与验证,从而在一定程度上缓解状态空间爆炸的情形。本文的主要贡献如下:(1)基于AADL语言的扩展机制,提出了一个能够支持精化行为建模的附属语言RBML,并给出它的语法和语义。该语言创新性地引入了自定义机制,用来提升行为建模时的灵活性。它允许用户根据需要在RBML规范中定义变量、方法和约束,以描述AADL核心语言所不能表达的数据、行为和需求。(2)定义了RBML语言到Z3求解器的转换规则并设计了主要的转换算法。本文选择了Z3求解器作为验证工具,可以在提升验证效率的同时有效地缓解状态空间爆炸的问题。本文还使用了OpenModelica工具对RBML规范中的连续行为进行仿真,来增强验证结果的可靠性。(3)设计并实现了一个工具链,用于支持RBML语言的建模、验证和仿真。本文实现了RBML语言在OSATE平台上的集成,允许用户在AADL模型中插入RBML附属规范以支持精化行为建模。此外,本文还开发了一个模型转换工具AADL2ZAO,用于将AADL模型自动转换为对应的形式化规范。该工具还与Z3和OpenModelica建立了连接,以便对转换生成的规范进行验证和仿真。本文以百度Apollo自动驾驶系统为例,说明了RBML语言在安全关键系统的行为建模与分析中的具体应用。实验结果表明,本文提出的方法能够有效地建模和分析行为的实现细节,从而保证功能设计的正确性以及整个系统的安全性。
基本信息
题目 | RBML:面向安全关键混成系统的精化行为建模语言 |
文献类型 | 硕士论文 |
作者 | 陈张涛 |
作者单位 | 华东师范大学 |
导师 | 刘静 |
文献来源 | 华东师范大学 |
发表年份 | 2020 |
学科分类 | 信息科技 |
专业分类 | 计算机软件及计算机应用 |
分类号 | TP311.52 |
关键词 | 精化行为建模,安全关键系统,模型验证,求解器 |
总页数: | 82 |
文件大小: | 5620K |
论文目录
摘要 |
Abstract |
第一章 绪论 |
1.1 研究背景和意义 |
1.2 技术路线及研究内容 |
1.3 国内外研究现状 |
1.4 论文组织 |
第二章 相关理论 |
2.1 AADL语言 |
2.2 Z3 求解器 |
2.3 Modelica语言 |
2.4 本章小结 |
第三章 精化行为建模语言RBML |
3.1 RBML语言的数据类型 |
3.2 RBML语言的语法 |
3.3 RBML语言的语义 |
3.4 温度控制系统的应用实例 |
3.5 本章小结 |
第四章 RBML精化行为模型的验证与仿真 |
4.1 模型转换的原理 |
4.2 RBML到 SMT-LIB的转换规则 |
4.3 RBML到 Modelica的转换规则 |
4.4 RBML语言的模型转换算法 |
4.5 本章小结 |
第五章 AADL2ZAO工具的设计与实现 |
5.1 RBML语言的元模型构建 |
5.2 AADL2ZAO工具的框架设计 |
5.3 AADL2ZAO工具的实现细节 |
5.4 本章小结 |
第六章 案例研究与方法对比 |
6.1 百度Apollo系统介绍 |
6.2 Apollo系统的RBML建模 |
6.3 离散行为的Z3 验证 |
6.4 连续行为的Modelica仿真 |
6.5 方法对比与性能分析 |
6.6 本章小结 |
第七章 总结与展望 |
7.1 总结 |
7.2 展望 |
参考文献 |
致谢 |
研究成果 |
相似文献
[1]人群聚集行为建模及仿真技术的研究[D]. 张子龙.天津理工大学2019 |
[2]基于行为树的CGF行为建模研究[D]. 付延昌.国防科学技术大学2016 |
[3]基于多智能体的人群行为建模及仿真研究[D]. 柴程.西安电子科技大学2018 |
[4]基于Swarm的模拟电磁机制的蜂群觅食行为建模与仿真[D]. 杜易霖.太原科技大学2016 |
[5]情感智能体认知行为建模研究[D]. 陈伟.国防科学技术大学2011 |
[6]基于有限自动机的软件行为建模方法的研究[D]. 周银.北京理工大学2011 |
[7]武警部队处置突发事件行为建模与实现技术研究[D]. 郑延军.国防科学技术大学2008 |
[8]群体组织协同行为建模语言解释器与应用描述方法研究[D]. 杨志谋.国防科学技术大学2006 |
[9]基于隐马尔可夫模型的自我调节学习行为建模研究[D]. 张晓彤.华中师范大学2020 |
[10]行人同伴群交通行为建模与仿真分析[D]. 栾庆熊.昆明理工大学2015 |
RBML:一种用于安全关键型混合系统的完善的行为建模语言
下载Doc文档