铁路计算机应用
鐵路計算機應用
철로계산궤응용
RAILWAY COMPUTER APPLICATION
2014年
7期
43-47
,共5页
临时限速%CTC分界口%信息交互%实时性%时间自动机%UPPAAL
臨時限速%CTC分界口%信息交互%實時性%時間自動機%UPPAAL
림시한속%CTC분계구%신식교호%실시성%시간자동궤%UPPAAL
temporary speed ristriction(TSR)%boundary area of CTC%information interaction%real-time performance%timed automata%UPPAAL
临时限速是高速铁路列控系统的重要组部分,CTC行车调度台分界口处的临时限迷信息交互频繁,对实时性的要求也更苛刻.为满足其实时性要求,采用时间自动机理论,结合分界口处临时限速相邻设备间的交互过程,分别建立各设备的时间自动机模型,通过时间自动机的积构建整个交互系统的网络模型,并利用UPPAAL验证工具对模型的功能和性能属性进行形式化验证.验证结果确认了交互过程中系统的安全性和受限活性.
臨時限速是高速鐵路列控繫統的重要組部分,CTC行車調度檯分界口處的臨時限迷信息交互頻繁,對實時性的要求也更苛刻.為滿足其實時性要求,採用時間自動機理論,結閤分界口處臨時限速相鄰設備間的交互過程,分彆建立各設備的時間自動機模型,通過時間自動機的積構建整箇交互繫統的網絡模型,併利用UPPAAL驗證工具對模型的功能和性能屬性進行形式化驗證.驗證結果確認瞭交互過程中繫統的安全性和受限活性.
림시한속시고속철로렬공계통적중요조부분,CTC행차조도태분계구처적림시한미신식교호빈번,대실시성적요구야경가각.위만족기실시성요구,채용시간자동궤이론,결합분계구처림시한속상린설비간적교호과정,분별건립각설비적시간자동궤모형,통과시간자동궤적적구건정개교호계통적망락모형,병이용UPPAAL험증공구대모형적공능화성능속성진행형식화험증.험증결과학인료교호과정중계통적안전성화수한활성.
