| 运行时验证及其在列车运行控制系统中的应用 |
| |
| 引用本文： | 赵林,唐涛,徐田华,柴铭,李宪.运行时验证及其在列车运行控制系统中的应用[J].铁道学报,2011(12):65-71. |
| |
| 作者姓名： | 赵林 唐涛 徐田华 柴铭 李宪 |
| |
| 作者单位： | 北京交通大学轨道交通控制与安全国家重点实验室; |
| |
| 基金项目： | 国家重点实验室自主课题基金(RCS2008ZQ002;RCS2008ZZ005); 中央高校基本科研业务费专项基金(2011JBM322); 北京交通大学-泰雷兹集团国际合作项目(M&V-SCHS) |
| |
| 摘 要： | 运行时验证是一种将模型检验方法与测试相结合的轻量级验证技术,它能够有效地降低系统验证的复杂度,提供系统运行阶段的安全保障,因此在安全苛求系统的验证领域有着极其重要的应用。本文提出一种基于三值逻辑的有限轨迹LTL可执行语义,允许"真"和"假"以外的逻辑值来显式的刻画验证过程中可能出现的非确定性,从而使得验证的结果更加精确。针对新的LTL语义给出了基于公式重写的运行监控算法和近似优化策略,并结合欧洲列车运行控制系统的实例,分析探讨了该方法在轨道交通控制领域的应用。
|
| 关 键 词： | 模型检验 测试 多值逻辑 公式重写 列车运行控制系统 |
Runtime Verification and its Applications in Train Control Systems |
| |
| ZHAO Lin,TANG Tao,XU Tian-hua,CHAI Ming,LI Xian.Runtime Verification and its Applications in Train Control Systems[J].Journal of the China railway Society,2011(12):65-71. |
| |
| Authors: | ZHAO Lin TANG Tao XU Tian-hua CHAI Ming LI Xian |
| |
| Institution: | ZHAO Lin,TANG Tao,XU Tian-hua,CHAI Ming,LI Xian (State Key Laboratory of Rail Traffic Control and Safety,Beijing Jiaotong University,Beijing 100044,China) |
| |
| Abstract: | Runtime verification has emerged as a promising verification technique that bridges the gap between traditional testing and model checking.It supplements formal verification with more lightweight dynamic techniques when these techniques fail due to complexity of issues,and it has important applications in the field of safety critical systems verification.In this paper,we present a 3-valued executable semantics for finite trace LTL,which can express the uncertainty during the monitoring proces by allowing ad... |
| |
| Keywords: | model checking test multi-valued logic formula rewriting train control systems |
| 本文献已被 CNKI 等数据库收录！ |
|
