Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect

被引：4

作者：

Basile, Davide ^{[1
]}

Mazzanti, Franco ^{[1
]}

Ferrari, Alessio ^{[1
]}

机构：

[1] CNR, Formal Methods & Tools Lab ISTI, Pisa, Italy

来源：

FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2023 | 2023年 / 14290卷

关键词：

umc; sparx enterprise architect; formal verification; uml;

D O I：

10.1007/978-3-031-43681-9_1

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

The use of formal methods can reduce the time and costs associated with railway signalling systems development and maintenance, and improve correct behaviour and safety. The integration of formal methods into industrial model-based development tools has been the subject of recent research, indicating the potential transfer of academic techniques to enhance industrial tools. This paper explores the integration of an academic formal verification tool, UML Model Checker (UMC), with an industrial model-based development tool, Sparx Enterprise Architect (Sparx EA). The case study being analyzed is a railway standard interface. The paper demonstrates howformal verification techniques from academic tools can be integrated into industrial development practices using industrial tools, and how simulation in Sparx EA can be derived from traces generated by the UMC formal verification activity. From this experience, we derive a set of lessons learned and research challenges.

引用

页码：1 / 21

页数：21

共 60 条

[1]

3ds, Dassault Cameo Systems Modeler

[2] Formalizing UML State Machines for Automated Verification - A Survey [J].

Andre, Etienne ;

Liu, Shuang ;

Liu, Yang ;

Choppy, Christine ;

Sun, Jun ;

Dong, Jin Song .

ACM COMPUTING SURVEYS, 2023, 55 (13S)

[3]

Basile Davide, 2023, Zenodo, DOI 10.5281/ZENODO.7920448

[4] Static detection of equivalent mutants in real-time model-based mutation testing An Empirical Evaluation [J].

Basile, Davide ;

ter Beek, Maurice H. ;

Lazreg, Sami ;

Cordy, Maxime ;

Legay, Axel .

EMPIRICAL SOFTWARE ENGINEERING, 2022, 27 (07)

[5] Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer Applying Formal Methods to Railway Standard Interfaces [J].

Basile, Davide ;

Fantechi, Alessandro ;

Rosadi, Irene .

FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2021, 2021, 12863 :174-190

[6] Designing a Demonstrator of Formal Methods for Railways Infrastructure Managers [J].

Basile, Davide ;

ter Beale, Maurice H. ;

Fantechi, Alessandro ;

Ferrari, Alessio ;

Gnesi, Stefania ;

Masullo, Laura ;

Mazzanti, Franco ;

Piattino, Andrea ;

Trentini, Daniele .

LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: APPLICATIONS, ISOLA 2020, PT III, 2020, 12478 :467-485

[7] Modelling and Analysing ERTMS L3 Moving Block Railway Signalling with Simulink and UPPAAL SMC [J].

Basile, Davide ;

ter Beek, Maurice H. ;

Ferrari, Alessio ;

Legay, Axel .

FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2019, 2019, 11687 :1-21

[8] On the Industrial Uptake of Formal Methods in the Railway Domain A Survey with Stakeholders [J].

Basile, Davide ;

ter Beek, Maurice H. ;

Fantechi, Alessandro ;

Gnesi, Stefania ;

Mazzanti, Franco ;

Piattino, Andrea ;

Trentini, Daniele ;

Ferrari, Alessio .

INTEGRATED FORMAL METHODS, IFM 2018, 2018, 11023 :20-29

[9]

Belli D., 2022, LNCS, V1376, P164, DOI [10.1007/978-3-031-26236-4_14, DOI 10.1007/978-3-031-26236-4_14]

[10] Extending SYSML with Refinement and Decomposition Mechanisms to Generate EVENT-B Specifications [J].

Bougacha, Racem ;

Laleau, Regine ;

Collart-Dutilleul, Simon ;

Ben Ayed, Rahma .

THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2022, 2022, 13299 :256-273

← 1 2 3 4 5 6 →