Techniques for modelling and verifying railway interlockings

被引：31

作者：

James, Phillip ^{[1
]}

Moller, Faron ^{[1
]}

Hoang Nga Nguyen ^{[1
]}

Roggenbach, Markus ^{[1
]}

Schneider, Steve ^{[2
]}

Treharne, Helen ^{[2
]}

机构：

[1] Swansea Univ, Swansea, W Glam, Wales

[2] Univ Surrey, Guildford GU2 5XH, Surrey, England

来源：

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER | 2014年 / 16卷 / 06期

基金：

英国工程与自然科学研究理事会;

关键词：

Railway verification; CSP; B; Model checking; Safety; VERIFICATION;

D O I：

10.1007/s10009-014-0304-7

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We describe a novel framework for modelling railway interlockings which has been developed in conjunction with railway engineers. The modelling language used is CSP parallel to B. Beyond the modelling we present a variety of abstraction techniques which make the analysis of medium-to large-scale networks feasible. The paper notably introduces a covering technique that allows railway scheme plans to be decomposed into a set of smaller scheme plans. The finitisation and topological abstraction techniques are extended from previous work and are given formal foundations. All three techniques are applicable to other modelling frameworks besides CSP parallel to B. Being able to apply abstractions and simplifications on the domain model before performing model checking is the key strength of our approach. We demonstrate the use of the framework on a real-life, medium-size scheme plan.

引用

页码：685 / 711

页数：27

共 36 条

[1]

Abrial J.-R., 2010, MODELING EVENT B

[2]

Abrial Jean-Raymond, 1996, The B-Book - Assigning Programs to Meanings

[3]

[Anonymous], 2013, PROB ANIMATOR MODEL

[4]

Antoni M., 2011, 3 INT WORKSH DEP CON, pix

[5]

Bjorner D., 2003, CTS

[6]

Cimatti Alessandro, 2012, Computer Aided Verification. Proceedings 24th International Conference, CAV 2012, P378, DOI 10.1007/978-3-642-31424-7_29

[7]

Fantechi Alessandro, 2011, Computer Safety, Reliability, and Security. Proceedings 30th International Conference, SAFECOMP 2011, P383, DOI 10.1007/978-3-642-24270-0_28

[8] Model Checking Interlocking Control Tables [J].

Ferrari, Alessio ;

Magnani, Gianluca ;

Grasso, Daniele ;

Fantechi, Alessandro .

FORMS/FORMAT 2010: FORMAL METHODS FOR AUTOMATION AND SAFETY IN RAILWAY AND AUTOMOTIVE SYSTEMS, 2011, :107-115

[9]

Fowler M., 2010, Domain-Specific Languages

[10]

Haxthausen Anne E., 2012, Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies. Proceedings of the 5th International Symposium, ISoLA 2012, P261, DOI 10.1007/978-3-642-34032-1_25

← 1 2 3 4 →