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

Modeling and Analysis of Railway Crossing Based on Differential Dynamic Logic

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

We presented the analysis of railway crossing based on differential dynamic logic. When a train sends ap-proaching 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.