探析基于scade的cbtc区域控制器软件开发

《探析基于scade的cbtc区域控制器软件开发》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、北京交通大学硕士学位论文基于SCADE的CBTC区域控制器软件开发姓名：张路申请学位级别：硕士专业：交通信息工程及控制指导教师：王海峰201012中文摘要摘要：区域控制器(ZoneCon仃0ller-ZC)是基于通信列车运行控制系统(CommlmjcationsBasedTraillCon仃olsyStem．CBTC)系统的地面控制核心设备，负责列车移动授权的计算和运行安全保障。ZC是一个复杂庞大的安全关键系统，其软件开发在规范刻画、设计、验证等诸多方面面临挑战。近年来，基于模型的软件开发方法在安全关键领域逐渐被认可，本文研究基于SCADE模型的ZC软件开发方法，主要工作体

2、现在如下方面：(1)以轨道交通控制系统为背景，研究了安全关键性系统的相关安全标准，分析了模型驱动开发的优势，并介绍了SCADE模型开发工具。(2)研究了ScADE理论基础一同步编程理论。研究了LUSTRE语言的语法规则和LUSTRE语言对反应式系统的进行模型描述的抽象方法。分析了数据流图和安全状态机这两种形式化建模机制的语义基础、建模方法以及模型的特性。研究了同步编程理论对模型的两种确认方法模拟仿真和形式化验证。(3)采用ScADE模型工具，对zC进行建模。对ZC进行了形式化描述，建立ZC的SCADE总体模型。通过分析区域控制器控制列车的典型场景，将ZC的主要功能划分为列车

3、管理功能、进路匹配功能和MA计算功能，详细的设计了各功能的软件流程。采用安全自动机建模机制，建立了列车管理功能的模型；采用数据流建模机制，建立了进路匹配功能和MA计算功能的模型。(4)采用SCADE仿真与验证工具，对zC模型进行检验。采用故障模式及影响分析方法，对ZC的主要功能进行了安全分析。使用SCADE模拟仿真模块，对模型进行了测试，使用SCADE形式化验证器，对模型的安全属性进行了验证，从而确认了模型的正确性。通过对课题的研究，本文得出以下结论：基于SCADE模型的开发避免了对软件的重复性描述，避免了人工编写代码，能在系统设计初期发现设计缺陷，提高了软件质量和开发效率

4、。关键词：cBTC；ScADE；区域控制器；基于模型开发分类号：u284．48+2ABSTRACTABSTRAC’I!ZoneCon仃oller(ZC)ist11ecoregroundcon旬rolequipmentofCommuIlicationsBaLsedTraillCorl仃ol(CBTC)system．ZCisresponsibleforcalculatingmen面nmoVementautllori够ZCisahugecornplexs娟匆一耐ticalsystem，anditisdi伍clIlt)rtodes嘶be，t0desig玛aIldtOValidate

5、．Recently，model—b2Lsedsof}waredeVelopmentmemodisdsiI毽．Illmispaper'SCADEmodel．b嬲eddeVelopmentisusedforsofharedeVelopmentofZC．nlem痂workoftllispaperisasfollowS：1)Studymes疵t)rcriticalsystems锄drelatedsaf时咖dardsoftllerailtra伍ccon缸olsyStem．An删ysisonⅡlead、7绷胁gesofmodel-baSedso小varedeVelopmentisgiV

6、en．Thent11eSCADEtooll【itsare岫duced．2)TheoreticalbasisofSCADE，S)，Ilchronouspro野a加mingnleo巧isstudied．111e肿mmarrulesandmemodelofLUSTRElang吼gearedesc^bed．S疵statemachmaIldda组nowmodelisresearchedaS也emodels印proachofLUSTRE．nlensiIIlulationandfo册alVerificationaSthetwoV甜idationwaysofs”1chr0110uSpro矿

7、锄衄血gtlleo巧isresearched．3)111eSCADEmodelofZChaSbeenbuilt．SeVeral咖icalscen撕osofZonecon仃0llerareaIlalyzed．Them豳劬ctioIlSof恤Zonecon仃olleraredesigned．SCADEisuSedtobuildmernodelsoftllese劬ctionS．The仃ainmaIlagement劬ctionismodeledbys疵statemacIline；缸leroutematcllingandMA