安全关键混成系统建模与验证方法研究

发布时间：2024-01-29 21:48

　　如何对安全关键混成系统进行形式化建模及验证方法是一项重要的科学问题。在现有的工程实践中,作为验证对象的安全属性缺乏规范化的获取方式;工业应用广泛的形式化建模语言LUSTRE不支持对物理世界连续行为的建模;系统的高复杂度带来的状态空间爆炸问题使得验证无法完成。这些难点的存在阻碍着安全关键混成系统的安全性的进一步提高,已经成为了安全关键软件行业不可回避的挑战。本文以构建安全关键混成系统建模与验证方法为研究目标,从分析需求规约出发,针对形式化验证方法中模型检验方法的特征,提出了一套可行的规范化流程,主要贡献包括:·提出了安全关键混成系统建模及验证框架。该框架从需求规约出发,覆盖了对系统进行需求建模、需求分解、设计建模、验证实现等步骤,解决了从需求出发难以构建对系统进行验证所需的组件的问题。·提出了两种基于投影的问题分解方法。这两种方法都以问题框架方法为基础,分别从子需求和变量约束的角度寻找投影维度,对问题模型进行分解。从而降低了描述安全关键混成系统的问题的复杂度。·定义了混成系统建模语言Hybrid LUSTRE。该语言以同步建模语言LUS-TRE为基础,结合混成自动机时间模型,给出了形式化...

【文章页数】：111 页

【学位级别】：博士

【文章目录】：
内容摘要
Abstract
第一章 引言
    1.1 研究背景
    1.2 研究现状
        1.2.1 混成系统建模方法
        1.2.2 混成系统验证方法
    1.3 本文工作
    1.4 论文结构
第二章 工作基础
    2.1 混成系统
    2.2 模型检验
    2.3 同步建模语言LUSTRE
    2.4 问题框架方法
    2.5 本章小结
第三章 安全关键混成系统建模及验证框架
    3.1 框架概述
    3.2 建模方法
    3.3 验证系统建模方法
    3.4 本章小结
第四章 需求建模和需求分解
    4.1 需求建模
    4.2 基于子需求的问题分解方法
    4.3 基于约束的问题分解方法
        4.3.1 约束分类
        4.3.2 投影维度的选择
        4.3.3 基于约束的投影的定义
    4.4 本章小结
第五章 混成系统同步建模语言Hybrid LUSTRE
    5.1 语言设计
    5.2 Hybrid LUSTRE语法
        5.2.1 表达式
        5.2.2 节点
    5.3 Hybrid LUSTRE语义
        5.3.1 指称语义
        5.3.2 安全语义
        5.3.3 活性语义
    5.4 设计建模及实现
    5.5 本章小结
第六章 验证问题的需求建模到设计建模
    6.1 验证问题的需求建模
    6.2 验证问题的需求分解
        6.2.1 假设与理论依据
        6.2.2 基于子安全属性的验证问题分解
        6.2.3 基于约束的验证问题分解
    6.3 验证问题的设计建模及实现
    6.4 本章小结
第七章 基于通信的列车控制系统的建模与验证
    7.1 案例描述
    7.2 工具支持
    7.3 需求建模
        7.3.1 需求描述
        7.3.2 需求问题
    7.4 需求分解
        7.4.1 基于子属性的建模问题分解
        7.4.2 基于约束的建模问题分解
    7.5 设计建模及实现
        7.5.1 设计建模
        7.5.2 模型实现
    7.6 验证问题的建模与验证
        7.6.1 验证需求获取
        7.6.2 验证问题需求建模
        7.6.3 验证问题需求分解
    7.7 验证结果与评估
        7.7.1 验证耗时对比
        7.7.2 适用系统规模
        7.7.3 两种问题分解方法的对比
    7.8 本章小结
第八章 总结与展望
附录
参考文献
致谢
攻读博士学位期间发表论文和科研情况



本文编号：3888899