形式化方法在列车运行控制系统中的应用

被引：30

作者：

曹源 ^{[1
]}

唐涛 ^{[1
]}

徐田华 ^{[1
]}

穆建成 ^{[2
]}

机构：

[1] 北京交通大学轨道交通控制与安全国家重点实验室

[2] 铁道部科学技术司

来源：

交通运输工程学报 | 2010年 / 10卷 / 01期

基金：

高等学校博士学科点专项科研基金;

关键词：

交通信息工程; 形式化方法; 列车运行控制系统; 安全苛求系统;

D O I：

10.19818/j.cnki.1671-1637.2010.01.020

中图分类号：

TP273 [自动控制、自动控制系统];

学科分类号：

080201 ; 0835 ;

摘要：

为了确保列车运行控制系统设计和开发的正确性,比较了仿真、测试和形式化3种能够验证系统设计正确性的方式。根据列车运行控制系统对安全的苛求性,提出了4个与系统安全相关的重要特性,即实时性、混成性、分布(并发)性、反应性,并分析了与这些特性相关的具体形式化方法。通过对每种形式化方法的数学基础和应用范围的分析和归类,给出了各种方法的优势和不足。分析结果表明:任何形式化方法的应用都具有一定的局限性,这是由模型检验和定理证明的本质所决定的;指出了新方法提出、既有方法拓展以及多方法集成将是列车运行控制系统的形式化领域的方向。

引用

页码：112 / 126

页数：15

共 9 条

[1] 使用延时演算的时间化RSL的指称语义(英文) [J].

李黎 ;

何积丰 .

软件学报, 2001, (06) :802-815

[2] 时段演算综述 [J].

李晓山，周巢尘 .

计算机学报, 1994, (11) :842-851

[3]

轨道交通列车运行控制系统的形式化建模和模型检验方法研究[D]. 燕飞.北京交通大学 2006

[4]

Automatic Verification of Combined Specifications: An Overview[J] . Ernst-Rüdiger Olderog.Electronic Notes in Theoretical Computer Science . 2008

[5]

Model checking Duration Calculus: a practical approach[J] . Roland Meyer,Johannes Faber,Jochen Hoenicke,Andrey Rybalchenko.Formal Aspects of Computing . 2008 (4)

[6]

Atemporal dynamic logic for verifying hybridsystem invariants. PLATZER A. Logical Foundations of ComputerScience：international symposium . 2007

[7]

Modelling a distributedrailway control system. MADSEN M S,MARTIN M B. TechnicalUniversity of Denmark . 2005

[8]

The Kluwer International Series inEngineering and Computer Science. KAPUR D,WI NTER V L. Kluwer AcademicPublishing . 2001

[9]

A domain specificlanguage for rail way control systems. HAXTHAUSEN A E,PELESKA J. Proceedings of the Sixth Biennial WorldConference on Integrated Design and Process Technology . 2002

← 1 →