RBML:一种用于安全关键型混合系统的完善的行为建模语言

RBML:一种用于安全关键型混合系统的完善的行为建模语言

随着功能需求的不断增加,安全关键系统的设计变得越来越复杂。如何通过建模与验证的方法保证安全关键系统的质量,一直以来都是形式化方法领域备受关注的问题。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文档

猜你喜欢