学位论文 > 优秀研究生学位论文题录展示

CTCS-3级列控系统的UML建模与模型检验研究

作　者: 吴晓丹
导　师: 宁滨
学　校: 北京交通大学
专　业: 交通信息工程及控制
关键词: CTCS-3 UML 符号模型检验 SMV 故障注入
分类号: TP273
类　型: 硕士论文
年　份: 2010年
下　载: 90次
引　用: 0次
阅　读: 论文下载

内容摘要

CTCS-3级列车运行控制系统是基于GSM-R无线传输系统实现安全控制信息双向传输的列车运行控制系统,是中国列车控制系统的重要组成部分。为了实现客运专线列车运行控制系统的国产化,必须研究适用于客运专线的CTCS3级技术规范和关键技术,形成中国高速客运专线列车运行控制系统的技术体系。在系统开发中,建立模型是研究系统的重要手段和前提。建立的模型首先必须易于开发人员理解和使用,其次模型必须正确地反映系统的需求,最后列车运行控制系统模型的安全性也是一个需要关注的问题。UML是一种通用可视化建模语言,易于理解和掌握因而适合于团队开发。然而UML本身没有提供验证模型正确性的手段,因此需要采用其他方法对UML模型进行检验。符号模型检验技术是形式化验证中很重要的一种方法,适用范围广、速度快且充分自动化。本文利用符号模型检验系统对UML模型进行检验。在模型检验的基础上本文得出了系统的SMV模型,之后利用故障注入技术对得到的SMV模型进行了相关的安全性分析。首先,本文对CTCS-3级列控系统级间转换场景进行了分析,然后对其进行UML建模得到UML类图和UML状态图。UML类图给类增加了表示系统组成之间信息交互的输入输出事件,UML状态图主要表示对象在输入事件的触发下发生状态转移并产生输出事件。在对建立好的UML模型进行检验之前,需要把UML模型转换为SMV模型。UML类图中的每个类在SMV模型中对应的是它的一个SMV模块,而类所对应的对象的状态转移则由相应的SMV模块中状态变量的更新来表达。本文在转换中建立了转换的一般规则。符号模型检验中,系统性质是用计算树逻辑公式CTL表达的。把系统的SMV模型和系统性质输入符号模型检验系统就可以检验系统性质如可达性、活性等。检验结果为True,则说明系统满足给出的性质；检验结果为False,则说明SMV模型或UML模型存在错误,可以根据反例进行相应的分析。在对系统的SMV模型修改使其满足所有给出的性质后,可以利用故障注入技术把故障注入到SMV模型中。系统的安全性质同样可以通过CTL公式来表达,之后就可以检验系统的安全性质。故障树的结构函数是一个布尔函数,利用SMV可以得到布尔函数的真值表并生成一个故障树。

全文目录

致谢  5-6
中文摘要  6-7
ABSTRACT  7-11
1 引言  11-20
  1.1 选题背景及意义  11-12
  1.2 CTCS-3级列控系统简介  12-14
  1.3 关键技术介绍  14-17
    1.3.1 UML建模技术  14-15
    1.3.2 符号模型检验系统  15
    1.3.3 故障注入技术  15-17
  1.4 形式化验证集成的研究现状  17
  1.5 论文研究内容及组织结构  17-20
2 CTCS-3级列控系统的UML建模  20-31
  2.1 场景描述  20-23
    2.1.1 概述  20
    2.1.2 级间转换过程  20-22
    2.1.3 级间转换过程UML顺序图  22-23
  2.2 建立UML模型  23-31
    2.2.1 建立UML类图  24-26
    2.2.2 建立UML状态图  26-31
3 UML模型转换为SMV模型  31-43
  3.1 SMV语言介绍  31-33
  3.2 转换UML模型  33-43
    3.2.1 转换Balise类  33-37
    3.2.2 转换External_Event类  37-38
    3.2.3 转换OnBoardEquipment类  38-40
    3.2.4 Main模块  40-43
4 使用SMV检验系统性质  43-53
  4.1 计算树逻辑公式介绍  43-45
  4.2 检验SMV模型  45-49
  4.3 遇到的问题  49-53
5 SMV模型的安全性分析  53-67
  5.1 基于故障注入的安全性分析  53-62
  5.2 符号化故障树分析  62-67
    5.2.1 利用SMV生成故障树  62-65
    5.2.2 小结  65-67
6 总结与展望  67-68
参考文献  68-71
作者简历  71-73
学位论文数据集  73

CTCS-3级列控系统的UML建模与模型检验研究

内容摘要

全文目录

相似论文