基于微分动态逻辑的铁路道口控制分析

计算机科学 ›› 2013, Vol. 40 ›› Issue (10): 231-234.

基于微分动态逻辑的铁路道口控制分析

钱磊,郁文生

华东师范大学上海高可信计算重点实验室上海200062;华东师范大学上海高可信计算重点实验室上海200062

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本文受国家自然科学基金项目(61070048),国家自然科学基金委员会创新研究群体科学基金项目(61021004),国家“863”计划项目(2011AA010101),国家“973”计划项目(2011CB302802),上海市重点学科建设项目(B412),上海市教育委员会科研创新项目(11ZZ37)资助

Modeling and Analysis of Railway Crossing Based on Differential Dynamic Logic

QIAN Lei and YU Wen-sheng

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

摘要： 利用微分动态逻辑对铁路道口控制进行形式化分析与建模。在火车从发送接近信号到进入道口的运动过程中,根据火车到达道口时间上的要求,将火车速度控制问题抽象成一个混成系统的安全性性质,用微分动态逻辑来描述,并使用混成系统证明工具KeYmaera对系统的安全性进行验证,以实现对火车进入道口前速度的正确控制。

关键词: 微分动态逻辑,铁路道口控制,混成系统,形式化验证

Abstract: We presented the analysis of railway crossing based on differential dynamic logic． When a train sends approaching signal and goes into the crossing,the limit of time spending in this period helps us identify safe ranges for the train speed control．We also illustrated modeling of this hybrid system using hybrid program and differential dynamic logic．Using the theorem prover KeYmaera,we formally verified hybrid safety properties of Railway Crossing about the train,and obtained the right speed control condition.

Key words: Differential dynamic logic,Railway crossing control,Hybrid system,Formal verification

钱磊,郁文生. 基于微分动态逻辑的铁路道口控制分析[J]. 计算机科学, 2013, 40(10): 231-234. https://doi.org/

QIAN Lei and YU Wen-sheng. Modeling and Analysis of Railway Crossing Based on Differential Dynamic Logic[J]. Computer Science, 2013, 40(10): 231-234. https://doi.org/

参考文献

[1] Schaft A V D,Schumacher H．An Introduction to Hybrid Dy-namical System [M]．London:Spring-Verlag,2000
[2] Loos S M,Platzer A．Safe intersections:At the crossing of hybrid systems and verification[C]∥14th International IEEE Conference on Intelligent Transportation Systems,2011．Washington,DC,USA:Kyongsu Yi,2011:1181-1186
[3] Loos S M,Platzer A,et al．Adaptive cruise control:Hybrid,distributed,and now formally verified[C]∥17th International Symposium on Formal Methods,2011．Limerick,Ireland:Sprin-ger,2011,volume 6664of LNCS,42-56
[4] Platzer A,Quesel J．Logical verification and systematic parametric analysis in train control:Hybrid Systems:Computation and Control[C]∥11th International Conference,2008．St．Louis,USA:Springer,2008,volume 4981of LNCS,646-649
[5] Platzer A．Differential-algebraic dynamic logic for differential-algebraic programs [J]．Journal of Logic and Computation,2010,20(1):309-352
[6] Platzer A．Logical Analysis of Hybrid Systems:Proving Theorems for Complex Dynamics [M]．London New York:Springer,2010
[7] Platzer A,Quesel J．KeYmaera:A hybrid theorem prover for hybrid systems:Automated Reasoning[C]∥Fourth International Joint Conference,2008．Sydney,Australia:Springer,2008,vo-lume 5195of LNCS,171-178
[8] Platzer A．Differential dynamic logic for hybrid systems[J]．Journal of Automated Reasoning,2008,1(2):143-189
[9] Beckert B,Hahnle R,et al．Verification of Object-Oriented Software:The KeY Approach [M]．Berlin,Heidelberg:Springer,2007

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed