| 形式化方法在列车运行控制系统中的应用 |
| |
| 引用本文： | 曹源,唐涛,徐田华,穆建成.形式化方法在列车运行控制系统中的应用[J].交通运输工程学报,2010(1). |
| |
| 作者姓名： | 曹源 唐涛 徐田华 穆建成 |
| |
| 作者单位： | 北京交通大学轨道交通控制与安全国家重点实验室;铁道部科学技术司; |
| |
| 基金项目： | 国家自然科学基金项目(60634010,60736047);;“十一五”国家科技支撑计划项目(2006BAG02B04);;轨道交通控制与安全国家重点实验室自主研究课题(RCS2008ZZ005);;高等学校博士学科点专项科研基金项目(20070004005) |
| |
| 摘 要： | 为了确保列车运行控制系统设计和开发的正确性,比较了仿真、测试和形式化3种能够验证系统设计正确性的方式。根据列车运行控制系统对安全的苛求性,提出了4个与系统安全相关的重要特性,即实时性、混成性、分布(并发)性、反应性,并分析了与这些特性相关的具体形式化方法。通过对每种形式化方法的数学基础和应用范围的分析和归类,给出了各种方法的优势和不足。分析结果表明:任何形式化方法的应用都具有一定的局限性,这是由模型检验和定理证明的本质所决定的;指出了新方法提出、既有方法拓展以及多方法集成将是列车运行控制系统的形式化领域的方向。
|
| 关 键 词： | 交通信息工程 形式化方法 列车运行控制系统 安全苛求系统 |
Application of formal methods in train control system |
| |
| Institution: | 1.State Key Laboratory of Rail Traffic Control and Safety/a>;Beijing Jiaotong University/a>;Beijing 100044/a>;China |
| |
| Abstract: | To ensure the correctness of train control system design and development,the ways of simulation,test and formalization were compared.According to the safe critical attribute of train control system,the characters related to system safety were propounded such as real time,hybrid,distribution(concurrence) and reactivity,and the specific formal methods associated with every character were introduced in details.The analysis and classification of the methods were done based on their mathematical basis and applic... |
| |
| Keywords: | traffic information engineering formal method train control system safe critical system |
| 本文献已被 CNKI 等数据库收录！ |
