| 基于XML的时间自动机状态可达性分析在RBC子系统中的应用 |
| |
| 引用本文： | 宋海锋,;唐涛,;李开成,;吕继东.基于XML的时间自动机状态可达性分析在RBC子系统中的应用[J].铁路计算机应用,2014,23(6):10-15. |
| |
| 作者姓名： | 宋海锋 ;唐涛 ;李开成 ;吕继东 |
| |
| 作者单位： | 北京交通大学轨道交通运行控制系统国家工程研究中心,北京,100044%北京交通大学 轨道交通控制与安全国家重点实验室,北京,100044 |
| |
| 基金项目： | 国际863计划项目（2012AA112800）;轨道交通控制与安全国家重点实验室（北京交通大学）开放课题基金资助（RCS2011K010）;中央高校基本科研业务费专项资金资助（2012JBM024）. |
| |
| 摘 要： | 时间自动机中的状态可达性分析是模型建立完成之后的一个重要验证工作,大多数时间自动机建模工具均为非开源代码,不能与实际系统进行有机的结合.本文以CTCS-3中的无线闭塞中心(RBC)1]为实际系统,提出基于XML的时间自动机状态可达性分析2],实现了建模工具与实际测试平台不同开发环境下的数据交互,为完善整个测试平台在理论方法与实际应用相结合方面提出一个较为可行的方法.
|
| 关 键 词： | 模型检验 CTCS-3 可达性分析 形式化建模 测试分析 |
| 收稿时间： | 2015-10-09 |
Reachability analysis of timed automata based on XML in RBC Sub-system |
| |
| Institution: | SONG Haifeng, TANG Tao, LI Kaicheng, LV Jidong ( 1. National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China; 2.State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044, China ) |
| |
| Abstract: | Reachability analysis was an important verification work after the model was built in timed automata, while most of the timed automata modeling tools were belong to non-open source software, which couldn＇t join with the real system. This paper used the RBC Sub-system of CTCS-3 as an example, proposed a method based on the XML to implement the reachability analysis of the timed automata model, as a result, it was available to transport data between different development environment, a more feasible methods were put forward to complete the testing platform in both theoretical method and practical application. |
| |
| Keywords: | model checking CTCS-3 reachability analysis formal modeling tested analysis |
| 本文献已被 维普 等数据库收录！ |
| 点击此处可从《铁路计算机应用》浏览原始摘要信息 |
| 点击此处可从《铁路计算机应用》下载免费的PDF全文 |
|
