基于模型检测的轨道交通运营场景安全性分析

发布时间：2017-08-21 12:45

  本文关键词：基于模型检测的轨道交通运营场景安全性分析

  更多相关文章： 模型检测 UPPAAL工具 时间自动机 可达性分析

【摘要】：轨道交通这样的实时系统对时间的要求及其严格,要保障轨道交通运营场景的安全性,就需要对运营场景进行安全检测,而保证系统安全性的关键任务就是实时系统的时间约束的满足性。针对此问题,模型检测技术得以应用,模型检测的原理是为系统建立模型,用时态逻辑表示需要检测的性质,然后用检测算法检测该模型是否满足性质。使用的检测工具是UPPAAL工具,根据检测步骤需要理解UPPAAL工具的模型时间自动机的构造及如何用规范语言表示性质,还要理解其检测算法的实现。本文针对轨道交通的运营场景之一的RBC切换场景进行验证,使用UPPAAL工具验证其切换过程中的安全性。对实时系统的绝大多数安全性和活性的检测,模型检测都是通过可达性分析算法来完成。可达性分析算法是模型检测的基础,由于时间自动机的时间约束而加速了状态空间爆炸,增加了可达性分析算法的复杂性。已存的时间自动机可达性分析算法,或是基于等价时间区域图(Region)、有界差分矩阵DBM)采用半符号时间约束结构的状态空间遍历分析方法；或是基于BDD结构采用全符号时间约束的状态空间遍历方法。这两类方法割裂了状态变迁表达与时间约束表达符号关联,难以应用大规模案例分析。本文的主要工作是：1)采用常用的检测工具是UPPAAL工具,对典型的轨道交通运营场景进行功能安全性和时间约束的安全性进行检测,从而能够实现系统模型的安全性分析。2)提出一种全符号的可达性分析方法,采用BDD结构统一表达时间自动机的状态变迁空间和时间约束,给出了在状态可达全符号运算的基础上时间约束的运算系列算法,并给出了单自动机、多自动机的可达算法。最后实例验证算法的正确性。通过这种方法,可以实现时间自动机的全符号化可达性分析,为全符号时间系统模型检测提供分析基础。
【关键词】：模型检测 UPPAAL工具 时间自动机 可达性分析
【学位授予单位】：青岛科技大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：U298
【目录】：

• 摘要3-4
• ABSTRACT4-8
• 1 前言8-13
• 1.1 研究背景和意义8-9
• 1.2 研究现状9-10
• 1.3 主要研究内容10-13
• 2 系统建模13-25
• 2.1 模型检测的介绍13-14
• 2.2 统一建模语言UML顺序图14-16
• 2.2.1 UML介绍14
• 2.2.2 UML顺序图14-15
• 2.2.3 UML顺序图的扩展15-16
• 2.3 实现工具UPPAAL16-20
• 2.3.1 UPPAAL介绍16-17
• 2.3.2 UPPAAL的检测步骤17-19
• 2.3.3 UPPAAL的检测语法19-20
• 2.4 时间自动机模型的理论基础20-23
• 2.4.1 有时间约束的转换系统20-21
• 2.4.2 时间自动机的语法和语义21
• 2.4.3 时间自动机积的构造21-23
• 2.5 UML顺序图到时间自动机模型的转换23-25
• 3 系统性质25-32
• 3.1 计算树时态逻辑CTL*25-27
• 3.2 CTL和LTL27-30
• 3.2.1 LTL27-28
• 3.2.2 CTL28-30
• 3.3 CTL和LTL的模型检测算法30-32
• 3.3.1 CTL的模型检测算法30
• 3.3.2 LTL的模型检测算法30-32
• 4 运营场景的安全验证32-45
• 4.1 CTCS-3级列控系统简介32
• 4.2 CTCS-3运营场景之RBC切换32-34
• 4.3 RBC切换场景的建模34-43
• 4.3.1 建立RBC切换场景的UML模型34-37
• 4.3.2 建立RBC切换场景的UPPAAL模型-时间自动机网络37-43
• 4.4 RBC切换场景的安全验证分析43-45
• 5 基于BDD的全符号化的可达性算法45-72
• 5.1 已有的半符号化可达性分析方法45-49
• 5.1.1 域自动机45-46
• 5.1.2 带自动机46-49
• 5.2 基于BDD的全符号化可达性算法49-63
• 5.2.1 BDD存储结构理论49-53
• 5.2.2 一种时间约束的BDD存储结构——DDD结构53-59
• 5.2.3 单时间自动机的可达性分析算法59-60
• 5.2.4 多时间自动机的可达性分析算法60-63
• 5.3 全符号化的可达性分析算法实例63-72
• 总结与展望72-73
• 参考文献73-77
• 致谢77-78
• 攻读学位期间发表的学术论文目录78
• 攻读学位期间参加的科研项目78-79

【相似文献】

中国期刊全文数据库 前4条

1 梅元媛;;使用模型检测器进行测试的方法研究[J];广西轻工业;2007年02期

2 陆公正,戎玫,张广泉;基于稠密时间的实时系统模型检测的一个应用[J];苏州大学学报(工科版);2005年02期

3 方忆湘;高婷;黄风山;;Pro/E环境下零件MBD模型检测信息的获取[J];组合机床与自动化加工技术;2013年09期

4 ;[J];;年期

中国重要会议论文全文数据库 前5条

1 高静;曹子宁;;基于空间逻辑和计算树逻辑的模型检测[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

2 许梅;曹子宁;;基于谓词μ演算和空间逻辑的模型检测算法研究[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

3 何青;骆翔宇;苏开乐;;对弈必胜策略的符号化模型检测[A];2006年全国理论计算机科学学术年会论文集[C];2006年

4 王飞明;胡元闯;董荣胜;;模型检测中状态爆炸及其优化策略研究[A];广西计算机学会2008年年会论文集[C];2008年

5 陈道喜;张广泉;陈冬火;;NSPK协议的Spin模型检测[A];2008年全国开放式分布与并行计算机学术会议论文集(下册)[C];2008年

中国博士学位论文全文数据库 前10条

1 江华;界程演算模型检测[D];贵州大学;2008年

2 林荣德;移动界程演算及模型检测应用的关键问题研究[D];华南理工大学;2010年

3 刘剑;传值进程与移动进程的模型检测方法[D];中国科学院研究生院（软件研究所）;2005年

4 刘志锋;模型检测中关键技术的研究及其应用[D];南京大学;2011年

5 朱维军;时间区间时序逻辑模型检测：理论、算法及应用[D];西安电子科技大学;2011年

6 尹良泽;基于SAT的组合迁移系统模型检测技术研究[D];清华大学;2014年

7 陈冬火;超协调时序逻辑及其模型检测方法[D];中国科学院研究生院（成都计算机应用研究所）;2006年

8 田聪;命题投影时序逻辑的判定性、复杂性、表达性及模型检测[D];西安电子科技大学;2010年

9 黄宏涛;基于懒惰切片的模型检测技术研究[D];哈尔滨工程大学;2012年

10 刘金卓;基于符号化模型检测的软件演化过程模型验证[D];云南大学;2013年

中国硕士学位论文全文数据库 前10条

1 李永亮;基于DNA计算的CTL模型检测方法研究[D];郑州大学;2015年

2 杨树峰;基于统计模型检测的无线传感器网络协议建模与分析[D];郑州大学;2015年

3 张兴兴;基于广义可能性测度的互模拟及CTL不动点语义[D];陕西师范大学;2015年

4 王彬;基于多值模型检测的SaaS应用测试及其自动化研究[D];陕西师范大学;2015年

5 王凯;基于模型检测多反例对软件进行调试[D];电子科技大学;2015年

6 邓楠轶;基于广义可能性测度的模型检测器GPoCheck的设计与实现[D];陕西师范大学;2015年

7 张恒;多值模型检测器的研究与实现[D];陕西师范大学;2015年

8 高毅;不同模型检测下信号并串转换模块功能建模的研究[D];电子科技大学;2014年

9 崔晓爽;基于GSTE模型检测的信号并串转换模块功能验证的研究[D];电子科技大学;2014年

10 许落汀;基于BDDs的离散实时时态逻辑RTCTL*的符号化模型检测及证据生成[D];华侨大学;2015年

，

本文编号：712983