论文部分内容阅读
在高可信系统软件的整个生命周期中,会因为系统的需求分析、软件设计、代码实现及运营维护等方面存在某些微小的漏洞而引发无可预计的损失。故而,在系统设计开发中、投入使用前,有必要对系统的属性进行形式化描述,并对该系统软件进行抽象,剔除无关紧要的过程,对关键过程进行形式化建模,再对该形式化模型进行检测,验证系统功能特性均能有效实现且安全稳定,从而保障系统功能的完整健硕。模型检测是运用数学方法进行自动化验证的一种技术,在许多领域都有所应用,其算法思想也在不断被拓展。本研究是以模型检测为基础,运用UPPAAL等模型检测工具进行建模与属性验证、分析高可信系统的安全性。对系统安全性有严苛要求的计算机系统,不仅包含有各种离散行为,还包含具有时间约束的连续行为。在此类实时系统的开发与建模中,目前较主流的做法是用半形式化的建模语言UML与时间自动机来建模。本文的主要工作内容有以下几部分:(1)对模型检测的基本原理及相关方法进行研究,对时间自动机模型展开深入研究,根据系统场景的半形式化描述,研究UML时序图与时间自动机模型之间转换。(2)对模型检测工具UPPAAL的功能结构、输入模型的语法及语义及工具使用进行深入研究,为实时高可信系统的形式化建模与安全性验证分析打下研究基础。(3)研究了我国CTCS-3级列控系统运营场景中列控中心的相关构成,对该场景进行深入分析,采用UML顺序图对CTCS-3级列控系统的RBC切换场景进行描述,根据UML时序图到时间自动机间的转化思路,将UML时序图转变为时间自动机模型,采用模型检测工具UPPAAL对列控系统运营场景的安全性进行分析与验证。(4)为了确保高可信系统系统的充分安全性,不仅需要研究系统在通常情况下的功能行为是否满足系统的安全性要求,还需要研究系统在带有单个故障和多个故障组合情形下系统的安全防护及故障安全方面的处理能力。鉴于此,提出基于多故障的模型检测安全性分析方法,并应用到铁路车站联锁系统的安全性分析与验证实践中,解决了系统安全性分析中的多故障注入问题及形式化安全需求规范的生成问题,拓展了系统功能的安全性分析途径,进一步提高了系统的安全性分析质量。本文的研究成果可为高可信系统软件的开发、系统的安全性分析与验证、系统的安全评估提供了较好的理论指导和技术支撑,对我国高速铁路、国防武器装备、航空航天等高可信领域的系统安全性保障具有广泛的应用价值。