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

Modeling and Analysis of Railway Crossing Based on Differential Dynamic Logic

作　　者：钱磊[1] 郁文生[1] 

机构地区：[1]华东师范大学上海高可信计算重点实验室,上海200062

出　　处：《计算机科学》2013年第10期231-234,共4页Computer Science

基　　金：国家自然科学基金项目(61070048);国家自然科学基金委员会创新研究群体科学基金项目(61021004);国家"863"计划项目(2011AA010101);国家"973"计划项目(2011CB302802);上海市重点学科建设项目(B412);上海市教育委员会科研创新项目(11ZZ37)资助

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

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

分 类 号：TP302.2[自动化与计算机技术—计算机系统结构]