保障计算机安全论文提纲

论文题目：列控安全计算机分区软件的形式化建模与验证方法研究

摘要：随着通信技术、控制技术和计算机技术在铁路领域的飞速进步和应用,列车运行控制系统（简称“列控系统”）不断向着综合化、模块化的方向发展。安全计算机作为列控系统的核心部件,承载其大部分的安全功能,是一个典型的安全苛求系统。现代安全计算机正由传统的电子机械密集型向着软件密集型逐步过渡,软件所占比例逐步上升,规模也越来越大,由此产生了模块化的概念。为了实现安全计算机的高容错能力,采用分区的方式实现不同分组的软件在时间和空间上互不影响,独立运行。由于分区软件具有并发性和共享性的特征,对系统安全性和可靠性带来了挑战。而形式化方法以形式或逻辑系统为基础,能够支持对计算机系统进行严格的建模和验证,在系统设计开发过程能够分析、处理、证明系统性质,提高和保障其可信性。论文阐述了列控安全计算机综合模块化的发展趋势、分区软件结构特性及管理机制,对列控安全计算机分区软件形式化研究作了梳理,根据安全计算机的建模需求,归纳总结了分区管理需要解决的安全性、实时性和可调度性三方面的研究重点。为了对这些指标进行定性和定量分析,本文从以下几个方面开展了研究:（1）论文针对并行程序安全性的问题,设计了基于事务内存的并发安全控制机制,利用并发分离逻辑设计了推理抽象机,并制订了推理规则。之后采用不变式证明方法对安全机制的可靠性进行推理验证,证明了该机制能保障并行程序的正确性。随后搭建了2乘2取2安全计算机平台,对并行应用操作共享内存的过程进行了安全性测试,验证了该安全控制机制可以保证并发安全地访问共享资源。（2）论文针对实时性的问题,对传统的时间Petri网进行拓展,考虑到非马尔科夫时间参数,提出了基于随机时间Petri网的建模方法,突破了列控系统Petri网模型要求时间参数为指数分布的限制。通过随机时间Petri网的定义和相关参数的引入,能够对非马尔科夫时间参数中的确定性分布、Erlang分布、超指数分布进行区分处理。为了利用随机时间Petri网模型进行实时性验证,提出了基于随机状态类的瞬态分析算法,通过随机状态树的构建和马尔科夫再生点的计算,对含有一般性分布的时间参数的模型进行瞬态分析。之后搭建了分区通信的随机时间Petri网模型,利用所提出的算法进行了实时性分析验证,对过程数据、消息数据和监督数据分别采用不同调度算法的时延进行了分析。随后利用2乘2取2安全计算机平台,结合开源实时以太网技术POWERLINK,对分区通信实时性能进行测试。（3）论文针对可调度性的问题,同样对传统的时间Petri网进行了拓展,提出了带有优先级时间Petri网的建模方法。针对时分多路复用全局调度和抢占固定优先级局部调度策略,克服了非确定性的执行时间和局部资源共享的难题,对包含有周期、偶发、抖动任务的双层调度机制进行了建模。并且提出了基于状态空间枚举的分析算法,识别从任务释放开始到任务结束的所有路径,提取最优完成时间和最差完成时间,检验任务截止时间是否满足,从而实现模型的可调度性分析。随后在2乘2取2安全计算机平台上,利用Vxworks的根任务调度实现了分区软件的调度,并对分区调度时刻信息进行了测试。最后在对全文工作和创新点总结的基础上,提出了下一步需要改进的地方和继续研究的问题。图37幅,表18个,参考文献116篇。

关键词：列车运行控制系统;安全计算机;分区软件;并发分离逻辑;随机时间Petri网;带优先级的时间Petri网

学科专业：交通信息工程及控制

致谢

摘要

ABSTRACT

术语表

1 引言

1.1 研究背景

1.2 安全计算机的综合模块化

1.2.1 安全计算机简介

1.2.2 安全计算机发展趋势

1.2.3 分区的概念及意义

1.3 形式化方法

1.3.1 形式化方法分类

1.3.2 形式化方法选择

1.4 选题意义

1.5 论文结构与写作安排

2 列控安全计算机分区软件研究综述

2.1 安全计算机分区软件

2.1.1 分区软件结构

2.1.2 分区隔离机制

2.1.3 分区软件特性

2.2 分区软件形式化研究的需求

2.2.1 形式化研究的必要性

2.2.2 分区软件的建模和验证需求

2.3 研究现状

2.3.1 形式化证明

2.3.2 时间Petri网

2.4 存在的问题

2.2.1 安全性方面

2.2.2 实时性方面

2.2.3 可调度性方面

2.5 本章小结

3 基于并发分离逻辑的分区并行程序安全性验证

3.1 并行程序安全性

3.2 基于事务内存的安全机制设计

3.3 并行程序安全机制验证

3.3.1 不变式证明

3.3.2 并发分离逻辑

3.3.3 安全性的验证方法

3.4 抽象机模型设计

3.5 推理规则的定义

3.6 可靠性证明

3.7 实验验证

3.7.1 平台搭建

3.7.2 验证结果与分析

3.8 本章小结

4 基于随机时间Petri网的分区通信实时性验证

4.1 分区通信

4.1.1 通信网络

4.1.2 通信管理机制

4.1.3 时延分析

4.1.4 数据类型

4.2 随机时间Petri网

4.2.1 随机Petri网相关概念

4.2.2 连续时间马尔科夫链的求解

4.2.3 网络性能关键参数的求解

4.2.4 随机时间Petri的定义

4.3 随机时间Petri网瞬态分析算法

4.3.1 随机状态类的定义

4.3.2 通过枚举类的状态空间分析

4.3.3 基于马尔科夫再生理论的瞬态概率的计算

4.3.4 算法实例及验证

4.4 分区通信模型建立

4.5 分区通信模型分析

4.5.1 参数选取及量化指标

4.5.2 结果分析

4.6 实验验证

4.6.1 平台搭建

4.6.2 验证结果与分析

4.7 本章小结

5 基于带有优先级时间Petri网的分区可调度性验证

5.1 实时调度

5.1.1 实时系统及相关概念

5.1.2 实时调度算法

5.2 分区调度的时域模型

5.3 带有优先级时间Petri网

5.3.1 定义

5.3.2 基于状态空间枚举的分析算法

5.4 双层调度模型建立

5.5 双层调度模型分析

5.5.1 复杂度分析

5.5.2 验证结果

5.6 实验验证

5.6.1 平台搭建

5.6.2 验证结果与分析

5.7 本章小结

6 结论

6.1 论文工作总结

6.2 未来工作展望

参考文献

图索引

表索引