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