计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2013年
z2期
94-97,130
,共5页
王瑾%孙景昊%何兴权%孟亚坤
王瑾%孫景昊%何興權%孟亞坤
왕근%손경호%하흥권%맹아곤
重载列车%安全监测%时间自动机%UppAal
重載列車%安全鑑測%時間自動機%UppAal
중재열차%안전감측%시간자동궤%UppAal
Heavy haul railway%Safety supervision%Timed automaton%UppAal
重载列车进港安全监测是我国港口信息化建设中的重点和难点问题.实现列车运行过程追踪自动化对于保证安全高效完成列车进港监测具有十分重要的作用.在速度触发的条件下,设计了能够实时感知人员攀车行为的低功耗信息物理系统,并基于时间自动机理论给出了该系统的实时行为模型.应用UppAal工具仿真了系统的运行轨迹,并验证了系统可达性、安全性、活性和实时性等系统关键性质.实验结果表明,系统不仅在逻辑上满足正确性,而且在任何系统状态上都不会对时间约束发生偏移性错误.
重載列車進港安全鑑測是我國港口信息化建設中的重點和難點問題.實現列車運行過程追蹤自動化對于保證安全高效完成列車進港鑑測具有十分重要的作用.在速度觸髮的條件下,設計瞭能夠實時感知人員攀車行為的低功耗信息物理繫統,併基于時間自動機理論給齣瞭該繫統的實時行為模型.應用UppAal工具倣真瞭繫統的運行軌跡,併驗證瞭繫統可達性、安全性、活性和實時性等繫統關鍵性質.實驗結果錶明,繫統不僅在邏輯上滿足正確性,而且在任何繫統狀態上都不會對時間約束髮生偏移性錯誤.
중재열차진항안전감측시아국항구신식화건설중적중점화난점문제.실현열차운행과정추종자동화대우보증안전고효완성열차진항감측구유십분중요적작용.재속도촉발적조건하,설계료능구실시감지인원반차행위적저공모신식물리계통,병기우시간자동궤이론급출료해계통적실시행위모형.응용UppAal공구방진료계통적운행궤적,병험증료계통가체성、안전성、활성화실시성등계통관건성질.실험결과표명,계통불부재라집상만족정학성,이차재임하계통상태상도불회대시간약속발생편이성착오.