Document - Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect

2023

Conference article Open Access

Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect

Basile D., Mazzanti F., Ferrari A.

UMC Sparx enterprise architect Formal verification UML

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 how formal 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.

Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 1–21, Antwerp, Belgium, 20-22/09/2023

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:485279,
	title = {Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect},
	author = {Basile D. and Mazzanti F. and Ferrari A.},
	doi = {10.1007/978-3-031-43681-9_1},
	booktitle = {FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 1–21, Antwerp, Belgium, 20-22/09/2023},
	year = {2023}
}