RBML：面向安全关键混成系统的精化行为建模语言

发布时间：2024-01-20 15:56

　　随着功能需求的不断增加,安全关键系统的设计变得越来越复杂。如何通过建模与验证的方法保证安全关键系统的质量,一直以来都是形式化方法领域备受关注的问题。AADL作为一种应用广泛的建模语言,在安全关键系统的设计与实现中发挥着重要的作用。它提供了丰富的组件用来描述系统的体系结构,并且能够支持性能关键属性的早期预测和重复性分析。然而,AADL描述系统行为的方式主要是基于自动机理论,在建模和验证大型复杂系统时难免会遇到状态空间爆炸问题。此外,由于缺乏描述行为细节的手段,AADL难以支持功能需求的分析与验证,从而无法保证整个系统的正确性和安全性。针对AADL语言在行为描述以及模型验证上的不足,本文提出了一种基于约束求解的精化行为建模方法。该方法扩展了AADL语言以增强其描述行为细节的能力,并且能够支持Z3求解器对构建的精化行为模型进行分析与验证,从而在一定程度上缓解状态空间爆炸的情形。本文的主要贡献如下:(1)基于AADL语言的扩展机制,提出了一个能够支持精化行为建模的附属语言RBML,并给出它的语法和语义。该语言创新性地引入了自定义机制,用来提升行为建模时的灵活性。它允许用户根据需要在RBML规范...

【文章页数】：82 页

【学位级别】：硕士

【文章目录】：
摘要
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 展望
参考文献
致谢
研究成果



本文编号：3881136