基于混成自动机的zc子系统安全的验证方法研究

《基于混成自动机的zc子系统安全的验证方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、学校代码：密级：公开硕士学位论文基于混成自动机的子系统安全的验证方法研究作者姓名侯晓鹏学科专业交通信息工程及控制指导教师黄友能副教授培养院系电子信息工程学院二零一五年四月硕士学位论文基于混成自动机的子系统安全的验证方法研究作者：侯晓鹏导师：黄友能北京交通大学年月学位论文版权使用授权书本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索，提供阅览服务，并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校向国家有关部门或机构送交论文的复印件和磁盘。学校可以为

2、存在馆际合作关系的兄弟高校用户提供文献传递服务和交换服务。保密的学位论文在解密后适用本授权说明）学位论文作者签名导师签名签字日期：年々月从日：糾年彳月日签字日期学校代码：密级：公幵北京交通大学硕士学位论文基于混成自动机的子系统安全的验证方法研究作者姓名：侯晓鹏学号：导师姓名：黄友能职称：副教授学位类别：工学学位级别：硕士学科专业：交通信息工程及控制研究方向：基于通信的列车控制北京交通大学年月致谢本论文是我在导师黄友能副教授的悉心指导下完成的，黄友能副教授严谨的治学态度和科学的工作方法给了我极大的帮助和影响。黄友能副教授悉心指导我完成了实验室的科研工

3、作，在学习上和生活上也给予了我很大的关心和帮助，在此衷心感谢三年来黄友能老师对我的关心和指导。吕继东、赵林老师，刘金涛博士对于我的科研工作和论文都提出了许多的宝贵意见，在此表示衷心的感谢。在实验室工作及撰写论文期间，任啸宇、张淼、阴加藤等同学对我论文及研究工作给予了热情帮助，在此向他们表达我的感激之情。最后向多年来一直理解和支持我的家人表达最深切的感谢和敬意，在漫长的求学生涯中，他们一如既往的关怀和鼓励，使我在人生的道路上一直保持乐观的心态和前进的动力。北京交通大学硕士学位论文摘要摘要近年来，随着城市化进程的加速，城市轨道交通业已经成为市内交通的首

4、选，用以缓解交通拥堵的情况。结合了通信技术，计算机技术与自动控制技术的基于通信的列车控制系统（是我国使用的城市轨道交通控制系统。作为一个安全苛求系统和复杂系统，在完成系统设计开发之后验证系统性质是否符合设计需求和寻找安全隐患是一项重要的任务。现阶段对于系统安全的分析验证主要利用传统的故障树等经典安全分析方法以及基于形式化模型的系统安全验证。本文从系统混成特性角度，利用线性混成自动机模型对子系统功能建模，验证子系统是否满足设计需求及行车安全。论文从系统原理及结构入手，总结出实时特性、安全特性、混合特性和并发特性四种系统具有的明显特征。目前对于实时与并

5、发特性的研究有利用通信顺序进程与时间自动机形式化方法建立系统模型并进行验证。针对子系统混成特性建模进行形式化验证的研究较少，混成特性关系到系统控制列车运行安全问题。本文提出利用线性混成自动机形式化方法对子系统进行建模分析与性质验证。文章选取扩展能力较强的统一建模语言（丨对系统进行描述，利用元素构造型、标记值和约束的扩展方式对顺序图进行了时间与变量方面扩展，表现系统的实时、并发和混合特性。根据模型转换理论，将扩展后的顺序图转换为线性混成自动机。通过制定严格的转换规则，保证模型转换过程中的模型一致性问题。线性混成自动机作为自动机的一个分支，能够描述离散

6、状态间连续变量的变化过程。本文最后选取了子系统中体现混成特性的列车跨越边界越区切换控制功能，结合移动授权生成过程进行建模，并利用混成自动机验证软件对模型性质与安全进行验证分析。证明了本文提出的子系统安全验证方法的可行性与正确性。关键词：基于通信的列车控制系统；子系统；形式化验证；混成自动机；模型转换；北京交通大学硕士学位论文，北京交通大学硕士学位论文：北京交通大学硕士学位论文目录目录弓丨研究背景及意义基于通信的列车控制系统（系统概述基于通信的列车控制系统简介系统的基本结构及特性分析系统安全的验证方法国内外现状研究内容及体系结构研究框架研究内容针对系

7、统特性的图描述与形式化方法分析针对系统特性的扩展基本概念语言扩展方式场景的规范顺序图建模针对系统特性的源模型扩展形式化方法分析形式化方法概述形式化规约与验证形式化分类本章小结混成自动机定义与模型转换规则制定模型转换概念及框架混成自动机概念混成自动机理论线性混成自动机定义线性混成模型定义实例转换定义与规则制定单元片段定义北京交通大学硕士学位论文目录单元片段转换规则组合片段转换规则本章小结区域控制中心及功能建模验证实例区域控制中心及列车管理区域控制中心列车管理跨越边界越区切换控制功能建模跨越边界越区切换控制功能场景分析跨越边界越区切换控制功能建模移动授

8、权生成过程及建模移动授权生成移动授权生成过程建模跨越边界越区切换控制功能模型验证线性混成自动机模型验证软件利用对跨越边界越