A Refinement-based Formal Development of Cyber-physical Railway Signalling Systems
A Refinement-based Formal Development of Cyber-physical Railway Signalling Systems
复制标题
基于细化的网络物理铁路信号系统形式化开发
DOI：
10.1145/3524052
复制
发表时间：
2023
影响因子：
1
通讯作者：
Aït-Ameur Y
中科院分区：
文献类型：
--
作者：
Aït-Ameur Y
多年来，形式化方法已成功地应用于铁路领域，形式化地证明了铁路系统的安全性。尽管如此，在正式方法领域几乎没有做什么来解决现代铁路信号系统的网络物理性质。在这篇文章中，我们提出了一种基于改进的建模和基于证据的验证的网络物理铁路信号系统的正式开发方法。我们的方法利用事件-B正式规范语言与混合系统和通信建模模式开发一个通用的混合铁路信号系统模型，可以进一步完善，以捕捉特定的铁路信号系统。这篇文章的主要技术贡献是细化的混合列车事件B模型与其他铁路信号子系统。网络物理铁路信号系统的完整模型被正式证明可以确保车辆安全分离并防止脱轨。此外，文章还展示了基于改进的网络物理系统开发方法的优势，该方法可以分解问题，从而减少验证和建模工作。
For years, formal methods have been successfully applied in the railway domain to formally demonstrate safety of railway systems. Despite that, little has been done in the field of formal methods to address the cyber-physical nature of modern railway signalling systems. In this article, we present an approach for a formal development of cyber-physical railway signalling systems that is based on a refinement-based modelling and proof-based verification. Our approach utilises the Event-B formal specification language together with a hybrid system and communication modelling patterns to developing a generic hybrid railway signalling system model that can be further refined to capture a specific railway signalling system. The main technical contribution of this article is the refinement of the hybrid train Event-B model with other railway signalling sub-systems. The complete model of the cyber-physical railway signalling system was formally proved to ensure a safe rolling stock separation and prevent their derailment. Furthermore, the article demonstrates the advantage of the refinement-based development approach of cyber-physical systems, which enables a problem decomposition and in turn reduction in the verification and modelling effort.
登录
查看更多内容
使用模型联合弥合非正式需求和正式规范之间的差距
DOI：
--
发表时间：
2018
期刊：
IEEE International Conference on Software Engineering and Formal Methods
影响因子：
--
作者：
F. R. Golra;F. Dagnat;J. Souquières;Imen Sayar;Sylvain Guérin
通讯作者：
Sylvain Guérin
DOI：
10.1007/978-3-642-10373-5_13
发表时间：
2009-11
期刊：
--
影响因子：
--
作者：
André Platzer;Jan-David Quesel
通讯作者：
André Platzer;Jan-David Quesel
DOI：
--
发表时间：
2010
期刊：
Verified Software: Theories, Tools, Experiments
影响因子：
--
作者：
M. Jastram;S. Hallerstede;M. Leuschel;Aryldo G. Russo
通讯作者：
Aryldo G. Russo
B 模型在集成验证框架中的嵌入认证
DOI：
--
发表时间：
2019
期刊：
Theoretical Aspects of Software Engineering
影响因子：
--
作者：
Alexandra Halchin;Y. A. Ameur;N. Singh;Abderrahmane Feliachi;J. Ordioni
通讯作者：
J. Ordioni
影响因子：
1.3
作者：
Berger, Ulrich;James, Phillip;Seisenberger, Monika
通讯作者：
Seisenberger, Monika