Techniques for modelling and verifying railway interlockings
Techniques for modelling and verifying railway interlockings
复制标题
DOI：
10.1007/s10009-014-0304-7
复制
发表时间：
2014-11
影响因子：
1.5
通讯作者：
Phillip James;F. Moller;N. H. Nga;M. Roggenbach;Steve A. Schneider;H. Treharne
中科院分区：
文献类型：
--
作者：
Phillip James;F. Moller;N. H. Nga;M. Roggenbach;Steve A. Schneider;H. Treharne
我们描述了一个新的框架，铁路联锁建模已与铁路工程师一起开发。使用的建模语言是CSPB。除了建模，我们提出了各种抽象技术，使分析中到大规模的网络可行。本文特别介绍了一种覆盖技术，允许铁路方案计划被分解成一组较小的方案计划。有限化和拓扑抽象技术是从以前的工作中延伸，并给出正式的基础。所有这三种技术都适用于CSPB以外的其他建模框架。能够在执行模型检查之前对领域模型应用抽象和简化是我们方法的关键优势。我们展示了使用的框架在现实生活中，中等规模的计划。
We describe a novel framework for modelling railway interlockings which has been developed in conjunction with railway engineers. The modelling language used is CSPB. 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 CSPB. 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.