基于SCR的安全关键系统需求归约与验证

发布时间：2022-11-03 20:32

　　安全关键系统是指那些系统失效会造成人员伤亡,环境和财产等的重大损失的软件系统。航空电子系统作为飞机上的核心系统,是典型的安全关键系统。需求分析是系统开发人员通过调研与分析,对用户和系统功能,性能等要求进行理解,并将非形式的需求描述转换为完整的需求定义的过程,是系统开发过程中最重要的阶段。但传统的需求表述方式由于自然语言的二义性,无法验证需求特性等问题使得需求容易出错,并且难以处理高度复杂的大型系统。基于形式化方法的需求归约过程以严格定义的语义和数学模型为基础,使得需求的表述更加清晰明了,易于理解,通过需求的自动化测试和检验工具的检验提高了需求的正确性和分析效率。但目前的形式化需求方法过于通用,工具普遍缺少安全属性的验证。本文以SCR（Software Cost Reduction）方法的研究为背景,针对传统的需求描述方法容易引入错误的问题,将SCR方法应用在飞机襟缝翼系统中,解决SCR方法过于通用性的问题,从保证系统安全性的角度出发,对基于SCR方法的检验工具T-VEC的功能进行扩展,增加安全属性验证的功能。具体研究内容如下所述:本文将形式化需求分析方法应用到安全关键性系统航空电子系统... 

【文章页数】：85 页

【学位级别】：硕士

【文章目录】：
摘要
abstract
第一章 绪论
    1.1 研究背景
    1.2 研究现状
        1.2.1 需求分析方法研究现状
        1.2.2 表格方法研究现状
    1.3 本文内容安排
第二章 背景知识
    2.1 SCR方法
        2.1.1 SCR方法的起源与发展
        2.1.2 SCR方法的理论基础及符号含义
        2.1.3 SCR方法需求归约流程
        2.1.4 SCR方法的优势
    2.2 T-VEC工具
        2.2.1 T-VEC工具简介
        2.2.2 T-VEC工具的使用及原理说明
        2.2.3 T-VEC工具的优劣
    2.3 模型检测
        2.3.1 模型检测基本思想
        2.3.2 时序逻辑
    2.4 本章小结
第三章 基于SCR方法的需求归约
    3.1 SCR方法应用过程
        3.1.1 系统需求归约
        3.1.2 系统设计归约
        3.1.3 软件需求归约
        3.1.4 系统容错能力
    3.2 SCR方法在襟缝翼控制单元的应用
        3.2.1 模块介绍
        3.2.2 模块需求归约
        3.2.3 模块设计归约
        3.2.4 模块软件需求归约
        3.2.5 故障处理及时间约束
    3.3 需求验证与分析
    3.4 方法总结
        3.4.1 监控变量与受控变量识别
        3.4.2 中间变量识别
        3.4.3 事件与条件的区分
        3.4.4 需求中变量间对应关系原则
    3.5 本章小结
第四章 T2N模型转换工具的设计与实现
    4.1 T-VEC与NuXMV语言
        4.1.1 T-VEC语言
        4.1.2 NuXMV语言
    4.2 T2N原型工具设计框架
        4.2.1 预处理
        4.2.2 词法和语法处理
        4.2.3 转换过程
    4.3 T2N原型工具的实现
        4.3.1 转换的硬件平台与语言
        4.3.2 转换规则定义
        4.3.3 转换实现算法
    4.4 本章小结
第五章 实例分析
    5.1 灯光控制系统描述与建模
        5.1.1 灯光控制系统介绍及选择依据
        5.1.2 系统建模过程
    5.2 实例验证与分析
        5.2.1 模型转换
        5.2.2 安全属性提取
        5.2.3 安全属性验证与结果分析
    5.3 本章小结
第六章 总结与展望
    6.1 研究总结
    6.2 未来工作展望
参考文献
致谢
在学期间的研究成果及发表的学术论文


【参考文献】：
期刊论文
[1]一种基于四变量模型的系统安全性建模与分析方法[J]. 胡军,石娇洁,程桢,陈松,王明明.  计算机科学. 2016(11)
[2]面向DO-333的襟缝翼控制单元安全性分析[J]. 陈光颖,黄志球,陈哲,阚双龙.  计算机科学. 2016(05)
[3]满足DO-178B要求的软件需求开发方法[J]. 陈鑫,王辉,牟明.  计算机工程与设计. 2012(07)
[4]软件需求的形式化转换模型[J]. 侯丽珍,蔡小娟,邹恒明.  计算机工程. 2007(05)



本文编号：3700579