文档介绍：北京交通大学
硕士学位论文
基于UML的CBTC系统区域控制器的建模与安全性验证
姓名:杨旭文
申请学位级别:硕士
专业:交通信息工程及控制
指导教师:王海峰
20080501
中文摘要摘要:基于通信的列车控制珻系统是利用连续、大容量的车地双向数字通信实现列车控制信息和列车状态信息传输的先进列车控制系统,是今后轨道交通列车运行控制系统的发展趋势。区域控制器,简称荂低车暮诵模杂τ萌砑杓频暮侠硇院安全性有很高的要求。论文首先介绍了系统区域控制器的基本原理和结构,根据安全苛求系统的“毙涂蚣埽庸δ苄枨蟮慕嵌热胧郑岷习踩ḿ扑慊教ǖ陌踩孕枨螅对区域控制器应用软件进行了详细的功能划分。并基于软件蓝图方法论进行了应用软件的设计,体现了结构化设计的特点。论文选择了统一建模语言捌淝度胧娇7⒒肪砇男问交模方法建立了系统区域控制器的模型,以区域控制器系统为模型主体,描述了区域控制器应用软件的系统模型,随后对子系统中发挥关键作用的功能模块进行了具体细化,完善整体功能。通过形式化的建模和分析,有效地排除了系统原有设计中存在的矛盾、二义性、含糊性等情况,保证区域控制器应用软件切实满足功能需求和安全性需求。论文最后在建立模型的基础上,通过将模型导入高安全性应用开发环境卸訸酉低秤τ萌砑纳杓平邢喙氐陌踩匝橹ぃü阅P的模拟仿真、形式验证以及覆盖率分析,验证了设计的安全性、功能的完备性以及模型的覆盖程度,为子系统的设计提供了理论依据,给应用软件设计的完善提供了参考和指导。关键词:;区域控制器;綥;话踩匝橹ぃ分类号:
,.,琧.:;,,,.;籗;··瑃琣瓹.,.,—.,琲’瑃.,琺;.篣
图索引图湫偷腃℃系统结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.开放系统⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯:⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..图焖倏7⒐獭子系统整体结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.图迦砑峁雇肌图枨蠓治觥图输入数据防护示意图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯子系统类图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯子系统顺序图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯子系统活动图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯子系统状态图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯计算类图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..计算活动图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..切换状态图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图模型检验的基本原理⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯问郊煅榈难橹ち鞒獭7⒃怼图形式验证工作原理⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图模型覆盖率工作流程⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯子系统的P汀图单列车计算仿真结果⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..图多车追踪计算仿真结果⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..图形式验证的迪帧图创建的诘恪图主节点的形式验证⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯计算模块的形式验证及结果⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图对模块的除零检测和溢出检测⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..图模型覆盖率分析初始情况⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图不完全的覆盖率分析⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图完整的模型覆盖率分析⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图覆盖率分析报告⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.图图砑芷凇的原理⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯。应用软件功能划分⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯。子系统功能模块的细化⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯子系统用例图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图创建专用于形式验证的工程⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯
表索引表乃牟阍DP吞逑到峁埂氖油己屯肌表煌油荚K刂涞牟糠止叵怠表独锻嫉耐骋挥锓ā
崎叼学位论文作者签名:才戤劬衅勿签字日期:幼曝年耛学位论文版权使用授权书。氰本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索,并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校向国家有关部门或机构送交论文的复印件和磁盘。C艿难宦畚脑诮饷芎笫视帽臼谌ㄋ得孑签期师日导字●●■
学位论文作者签名:懒虫文、年耞独创性声明本人声明所呈交的学位论文是本人在导师指导下进行的研究工作和取得的研究成