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.
Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect
Basile D;Mazzanti F;Ferrari A
2023
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
prod_485279-doc_200988.pdf
accesso aperto
Descrizione: Preprint - Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect
Tipologia:
Documento in Pre-print
Licenza:
Nessuna licenza dichiarata (non attribuibile a prodotti successivi al 2023)
Dimensione
1.25 MB
Formato
Adobe PDF
|
1.25 MB | Adobe PDF | Visualizza/Apri |
prod_485279-doc_201922.pdf
solo utenti autorizzati
Descrizione: Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect
Tipologia:
Versione Editoriale (PDF)
Licenza:
NON PUBBLICO - Accesso privato/ristretto
Dimensione
1.88 MB
Formato
Adobe PDF
|
1.88 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.