2026
Contribution to book
Open Access
Formal methods for railway systems: a survey of research and technology transfer projects
Basile Davide, Ter Beek Maurice Henri, Broccia Giovanna, Gnesi Stefania, Mazzanti Franco, Spagnolo Giorgio Oronzo, Bacherini Stefano, Becheri Carlo, Grasso Daniele, Magnani Gianluca, Tempestini Matteo, Zingoni Niccolò, Ferrari Alessio
This paper offers a retrospective on collaborative projects that involved Alessandro Fantechi and the authors over the past two decades, from the shared perspective of the Formal Methods and Tools (FMT) lab of the Italian National Research Council (CNR) and former collaborators at General Electric (GE) Transportation and Alstom. The focus is on research and technology transfer efforts in the field of formal methods for railway systems, where Alessandro Fantechi’s contributions have been central to the development and application of formal specification, model-based verification, and tool-supported analysis. Joint work in projects such as ASTRail, 4SECURail, and TRACE-IT, as well as in industrial collaborations with Alstom and GE Transportation Systems illustrates the sustained impact of these activities on both academic research and industrial practice. This contribution reflects on the evolution of these efforts, the formal methods adopted, and the outcomes achieved in terms of methodologies, tools, and integration into safety-critical development processes. It also highlights the collaborative environment fostered across institutions and organizations, which has been instrumental in advancing the use of formal methods in the railway domain.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. 31-54
DOI: 10.1007/978-3-032-12484-5_3
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Basile Davide, Ter Beek Maurice Henri, Broccia Giovanna, Gnesi Stefania, Mazzanti Franco, Spagnolo Giorgio Oronzo, Bacherini Stefano, Becheri Carlo, Grasso Daniele, Magnani Gianluca, Tempestini Matteo, Zingoni Niccolò, Ferrari Alessio
This paper offers a retrospective on collaborative projects that involved Alessandro Fantechi and the authors over the past two decades, from the shared perspective of the Formal Methods and Tools (FMT) lab of the Italian National Research Council (CNR) and former collaborators at General Electric (GE) Transportation and Alstom. The focus is on research and technology transfer efforts in the field of formal methods for railway systems, where Alessandro Fantechi’s contributions have been central to the development and application of formal specification, model-based verification, and tool-supported analysis. Joint work in projects such as ASTRail, 4SECURail, and TRACE-IT, as well as in industrial collaborations with Alstom and GE Transportation Systems illustrates the sustained impact of these activities on both academic research and industrial practice. This contribution reflects on the evolution of these efforts, the formal methods adopted, and the outcomes achieved in terms of methodologies, tools, and integration into safety-critical development processes. It also highlights the collaborative environment fostered across institutions and organizations, which has been instrumental in advancing the use of formal methods in the railway domain.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. 31-54
DOI: 10.1007/978-3-032-12484-5_3
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
CNR IRIS 
| link.springer.com | CNR IRIS 
| CNR IRIS
2025
Other
Open Access
Comparing model checking and model-based simulation: presentation
Basile D., Mazzanti F.
We use a railway-related case study to illustrate the differences that can be encountered while modeling and verifying a system using an academic formal verification framework and an industrial model-based framework. The different roles and structures of the two approaches are illustrated. We analyze instances where the exclusive use of interactive simulation cannot replicate the formal verification activity, and we derive some future research directions.Project(s): CN MOST (National Sustainable Mobility Centre) Spoke 4: Rail Transportation
Basile D., Mazzanti F.
We use a railway-related case study to illustrate the differences that can be encountered while modeling and verifying a system using an academic formal verification framework and an industrial model-based framework. The different roles and structures of the two approaches are illustrated. We analyze instances where the exclusive use of interactive simulation cannot replicate the formal verification activity, and we derive some future research directions.Project(s): CN MOST (National Sustainable Mobility Centre) Spoke 4: Rail Transportation
2025
Conference article
Open Access
Comparing model checking and model-based simulation
Basile D., Mazzanti F.
We use a railway-related case study to illustrate the differences that can be encountered while modeling and verifying a system using an academic formal verification framework and an industrial model-based framework. The different roles and structures of the two approaches are illustrated. We analyze instances where the exclusive use of interactive simulation cannot replicate the formal verification activity, and we derive some future research directions.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16236, pp. 135-154. Pisa, 26-28 Novembre 20205
DOI: 10.1007/978-3-032-10762-6_12
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Basile D., Mazzanti F.
We use a railway-related case study to illustrate the differences that can be encountered while modeling and verifying a system using an academic formal verification framework and an industrial model-based framework. The different roles and structures of the two approaches are illustrated. We analyze instances where the exclusive use of interactive simulation cannot replicate the formal verification activity, and we derive some future research directions.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16236, pp. 135-154. Pisa, 26-28 Novembre 20205
DOI: 10.1007/978-3-032-10762-6_12
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
CNR IRIS | link.springer.com | CNR IRIS | CNR IRIS
2024
Other
Restricted
CN MOST SP4 D1.3.1: Report on formal models
Basile D., Ter Beek M., Di Giandomenico F., Ferrari A., Mazzanti F., Chiaradonna S., Team Of Intesa San Paolo
In this deliverable, formal methods, model-based development, quantitative model-based analysis and their application to railway systems are discussed. Two applications are considered of, respectively, formal verification and quantitative model-based analysis: the formalization of railway interfaces, specifically focusing on the interface between two components of the European Railway Traffic Management System (ERTMS), and an uninterruptible power supply system.Project(s): CN MOST (National Sustainable Mobility Centre) Spoke 4: Rail Transportation
Basile D., Ter Beek M., Di Giandomenico F., Ferrari A., Mazzanti F., Chiaradonna S., Team Of Intesa San Paolo
In this deliverable, formal methods, model-based development, quantitative model-based analysis and their application to railway systems are discussed. Two applications are considered of, respectively, formal verification and quantitative model-based analysis: the formalization of railway interfaces, specifically focusing on the interface between two components of the European Railway Traffic Management System (ERTMS), and an uninterruptible power supply system.Project(s): CN MOST (National Sustainable Mobility Centre) Spoke 4: Rail Transportation
2023
Contribution to book
Open Access
A case study in formal analysis of system requirements
Belli D, Mazzanti F
One of the goals of the 4SECURail project has been to demonstrate the benefits, limits, and costs of introducing formal meth- ods in the system requirements definition process. This has been done, on an experimental basis, by applying a specific set of tools and method- ologies to a case study from the railway sector. The paper describes the approach adopted in the project and some considerations resulting from the experience.DOI: 10.1007/978-3-031-26236-4_14
Project(s): 4SECURAIL
Metrics:
Belli D, Mazzanti F
One of the goals of the 4SECURail project has been to demonstrate the benefits, limits, and costs of introducing formal meth- ods in the system requirements definition process. This has been done, on an experimental basis, by applying a specific set of tools and method- ologies to a case study from the railway sector. The paper describes the approach adopted in the project and some considerations resulting from the experience.DOI: 10.1007/978-3-031-26236-4_14
Project(s): 4SECURAIL
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | doi.org | CNR IRIS | CNR IRIS
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
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.DOI: 10.1007/978-3-031-43681-9_1
Project(s): 4SECURAIL, Sustainable Mobility National Research Center
Metrics:
Basile D, Mazzanti F, Ferrari A
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.DOI: 10.1007/978-3-031-43681-9_1
Project(s): 4SECURAIL
, Sustainable Mobility National Research CenterMetrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS
2023
Software
Metadata Only Access
Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect - Complementary data
Basile D, Mazzanti F, Ferrari A
This repository contains the UMC and SPARX EA data used in the paper: Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect by Davide Basile, Franco Mazzanti and Alessio Ferrari.DOI: https://doi.org/10.5281/zenodo.7920448
DOI: 10.5281/zenodo.7920448
Project(s): 4SECURAIL
Metrics:
Basile D, Mazzanti F, Ferrari A
This repository contains the UMC and SPARX EA data used in the paper: Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect by Davide Basile, Franco Mazzanti and Alessio Ferrari.DOI: https://doi.org/10.5281/zenodo.7920448
DOI: 10.5281/zenodo.7920448
Project(s): 4SECURAIL
Metrics:
See at:
CNR IRIS
2023
Conference article
Open Access
The 4SECURail case study on rigorous standard interface specifications
Belli D, Fantechi A, Gnesi S, Masullo L, Mazzanti F, Quadrini L, Trentini D, Vaghi C
In the context of the Shift2Rail open call S2R-OC-IP2-01- 2019, one of the two work streams of the 4SECURail project has pursued the objective to corroborate how a clear, rigorous standard interface specification between signaling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at illustrating some usable state-of-the-art techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments.DOI: 10.1007/978-3-031-43681-9_2
Project(s): 4SECURAIL
Metrics:
Belli D, Fantechi A, Gnesi S, Masullo L, Mazzanti F, Quadrini L, Trentini D, Vaghi C
In the context of the Shift2Rail open call S2R-OC-IP2-01- 2019, one of the two work streams of the 4SECURail project has pursued the objective to corroborate how a clear, rigorous standard interface specification between signaling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at illustrating some usable state-of-the-art techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments.DOI: 10.1007/978-3-031-43681-9_2
Project(s): 4SECURAIL
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS | CNR IRIS
2022
Journal article
Open Access
Efficient static analysis and verification of featured transition systems
Ter Beek Mh, Damiani F, Lienhardt M, Mazzanti F, Paolini L
A Featured Transition System (FTS) models the behaviour of all products of a Software Product Line (SPL) in a single compact structure, by associating action-labelled transitions with features that condition their presence in product behaviour. It may however be the case that the resulting featured transitions of an FTS cannot be executed in any product (so called dead transitions) or, on the contrary, can be executed in all products (so called false optional transitions). Moreover, an FTS may contain states from which a transition can be executed only in some products (so called hidden deadlock states). It is useful to detect such ambiguities and signal them to the modeller, because dead transitions indicate an anomaly in the FTS that must be corrected, false optional transitions indicate a redundancy that may be removed, and hidden deadlocks should be made explicit in the FTS to improve the understanding of the model and to enable efficient verification - if the deadlocks in the products should not be remedied in the first place. We provide an algorithm to analyse an FTS for ambiguities and a means to transform an ambiguous FTS into an unambiguous one. The scope is twofold: an ambiguous model is typically undesired as it gives an unclear idea of the SPL and, moreover, an unambiguous FTS can efficiently be model checked. We empirically show the suitability of the algorithm by applying it to a number of benchmark SPL examples from the literature, and we show how this facilitates a kind of family-based model checking of a wide range of properties on FTSs.Source: EMPIRICAL SOFTWARE ENGINEERING, vol. 27
DOI: 10.1007/s10664-020-09930-8
Metrics:
Ter Beek Mh, Damiani F, Lienhardt M, Mazzanti F, Paolini L
A Featured Transition System (FTS) models the behaviour of all products of a Software Product Line (SPL) in a single compact structure, by associating action-labelled transitions with features that condition their presence in product behaviour. It may however be the case that the resulting featured transitions of an FTS cannot be executed in any product (so called dead transitions) or, on the contrary, can be executed in all products (so called false optional transitions). Moreover, an FTS may contain states from which a transition can be executed only in some products (so called hidden deadlock states). It is useful to detect such ambiguities and signal them to the modeller, because dead transitions indicate an anomaly in the FTS that must be corrected, false optional transitions indicate a redundancy that may be removed, and hidden deadlocks should be made explicit in the FTS to improve the understanding of the model and to enable efficient verification - if the deadlocks in the products should not be remedied in the first place. We provide an algorithm to analyse an FTS for ambiguities and a means to transform an ambiguous FTS into an unambiguous one. The scope is twofold: an ambiguous model is typically undesired as it gives an unclear idea of the SPL and, moreover, an unambiguous FTS can efficiently be model checked. We empirically show the suitability of the algorithm by applying it to a number of benchmark SPL examples from the literature, and we show how this facilitates a kind of family-based model checking of a wide range of properties on FTSs.Source: EMPIRICAL SOFTWARE ENGINEERING, vol. 27
DOI: 10.1007/s10664-020-09930-8
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | ISTI Repository | CNR IRIS | CNR IRIS
2022
Conference article
Open Access
Formal modeling and initial analysis of the 4SECURail case study
Mazzanti F, Belli D
We present the case study developed in the context of the 4SECURail project and the approach used for its formal modeling and analysis. Starting from a simple SysML/UML behavioral model of the system requirements, three formal models have been developed using three different frameworks, namely UMC, ProB, and CADP/LNT. The paper shows how the different ways to represent and analyze the system from the three different points of view allow us to take advantage of the resulting diversity.Source: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, pp. 118-144. Munich, DE, 01/04/2022
DOI: 10.4204/eptcs.355.6
Project(s): 4SECURAIL
Metrics:
Mazzanti F, Belli D
We present the case study developed in the context of the 4SECURail project and the approach used for its formal modeling and analysis. Starting from a simple SysML/UML behavioral model of the system requirements, three formal models have been developed using three different frameworks, namely UMC, ProB, and CADP/LNT. The paper shows how the different ways to represent and analyze the system from the three different points of view allow us to take advantage of the resulting diversity.Source: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, pp. 118-144. Munich, DE, 01/04/2022
DOI: 10.4204/eptcs.355.6
Project(s): 4SECURAIL
Metrics:
See at:
eptcs.web.cse.unsw.edu.au | CNR IRIS | ISTI Repository | CNR IRIS
2022
Journal article
Open Access
FTS4VMC: a front-end tool for static analysis and family-based model checking of FTSs with VMC
Ter Beek Mh, Damiani F, Lienhardt M, Mazzanti F, Paolini L, Scarso G
FTS4VMC is a publicly available front-end tool for the static analysis and family-based model checking of a Featured Transition System (FTS). It can detect ambiguities in an FTS, disambiguate an ambiguous FTS, transform an FTS into a Modal Transition System (MTS), and interact with the VMC model checker for family-based verification.Source: SCIENCE OF COMPUTER PROGRAMMING, vol. 224
DOI: 10.1016/j.scico.2022.102879
Metrics:
Ter Beek Mh, Damiani F, Lienhardt M, Mazzanti F, Paolini L, Scarso G
FTS4VMC is a publicly available front-end tool for the static analysis and family-based model checking of a Featured Transition System (FTS). It can detect ambiguities in an FTS, disambiguate an ambiguous FTS, transform an FTS into a Modal Transition System (MTS), and interact with the VMC model checker for family-based verification.Source: SCIENCE OF COMPUTER PROGRAMMING, vol. 224
DOI: 10.1016/j.scico.2022.102879
Metrics:
See at:
CNR IRIS | ISTI Repository | www.sciencedirect.com | CNR IRIS | CNR IRIS
2022
Conference article
Open Access
The 4SECURail formal methods demonstrator
Mazzanti F, Belli D
The need for high-quality standard interfaces is widely recognized as a mandatory step to reduce procurement costs and create safely operating complex railway infrastructures. That is why European initiatives like EULYNX have been set up precisely with the purpose of supporting standard interfaces development. The exploitation of formal methods during the phase of standardization plays an essential role in raising the quality of the generated specifications. 4SECURail is a recent project that aims to precisely show, with a structured evaluation (known as the formal methods demonstrator), how formal methods might help to improve the quality of a specific signalling interface selected as case study. This paper describes the experience gained with the experiment.DOI: 10.1007/978-3-031-05814-1_11
DOI: 10.5281/zenodo.6245955
DOI: 10.5281/zenodo.6245956
Project(s): 4SECURAIL
Metrics:
Mazzanti F, Belli D
The need for high-quality standard interfaces is widely recognized as a mandatory step to reduce procurement costs and create safely operating complex railway infrastructures. That is why European initiatives like EULYNX have been set up precisely with the purpose of supporting standard interfaces development. The exploitation of formal methods during the phase of standardization plays an essential role in raising the quality of the generated specifications. 4SECURail is a recent project that aims to precisely show, with a structured evaluation (known as the formal methods demonstrator), how formal methods might help to improve the quality of a specific signalling interface selected as case study. This paper describes the experience gained with the experiment.DOI: 10.1007/978-3-031-05814-1_11
DOI: 10.5281/zenodo.6245955
DOI: 10.5281/zenodo.6245956
Project(s): 4SECURAIL
Metrics:
See at:
ZENODO | ZENODO | CNR IRIS | link.springer.com | ISTI Repository | doi.org | CNR IRIS | CNR IRIS
2022
Conference article
Open Access
The 4SECURail approach to formalizing standard interfaces between signalling systems components
Belli D, Fantechi A, Gnesi S, Masullo L, Mazzanti F, Pistilli G, Quadrini L, Trentini D, Vaghi C
In the context of the Shift2Rail open call S2R-OC-IP2-01-2019, one of the two work streams of the 4SECURail project (GA 881775) pursues the objective to corroborate how a clear, rigorous standard interface specification between signalling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at consolidating the most suitable techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments. This paper discusses the main results of the project.Source: TRANSPORTATION RESEARCH PROCEDIA. Lisbon, Portugal, 13-14/11/2022
Project(s): 4SECURAIL
Belli D, Fantechi A, Gnesi S, Masullo L, Mazzanti F, Pistilli G, Quadrini L, Trentini D, Vaghi C
In the context of the Shift2Rail open call S2R-OC-IP2-01-2019, one of the two work streams of the 4SECURail project (GA 881775) pursues the objective to corroborate how a clear, rigorous standard interface specification between signalling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at consolidating the most suitable techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments. This paper discusses the main results of the project.Source: TRANSPORTATION RESEARCH PROCEDIA. Lisbon, Portugal, 13-14/11/2022
Project(s): 4SECURAIL
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2021
Journal article
Open Access
Compositional verification of concurrent systems by combining bisimulations
Frédéric Lang F, Mateescu R, Mazzanti F
One approach to verify a property expressed as a modal ?-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes in a hierarchical way, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the Ldbr fragment? of the ?-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-preserving branching (divbranching for short) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or div-branching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend Ldbr with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems. In particular, we applied our approach to the verification problems of the RERS 2019 challenge and observed drastic reductions of the state space compared to the approach in which only strong bisimulation minimization is used, on formulas not preserved by divbranching bisimulation.Source: FORMAL METHODS IN SYSTEM DESIGN (DORDR., ONLINE)
DOI: 10.1007/s10703-021-00360-w
DOI: 10.1007/978-3-030-30942-8_13
Project(s): 4SECURAIL
Metrics:
Frédéric Lang F, Mateescu R, Mazzanti F
One approach to verify a property expressed as a modal ?-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes in a hierarchical way, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the Ldbr fragment? of the ?-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-preserving branching (divbranching for short) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or div-branching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend Ldbr with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems. In particular, we applied our approach to the verification problems of the RERS 2019 challenge and observed drastic reductions of the state space compared to the approach in which only strong bisimulation minimization is used, on formulas not preserved by divbranching bisimulation.Source: FORMAL METHODS IN SYSTEM DESIGN (DORDR., ONLINE)
DOI: 10.1007/s10703-021-00360-w
DOI: 10.1007/978-3-030-30942-8_13
Project(s): 4SECURAIL
Metrics:
See at:
hal.inria.fr | Formal Methods in System Design | CNR IRIS | link.springer.com | ISTI Repository | doi.org | Formal Methods in System Design | INRIA a CCSD electronic archive server | HAL Descartes | CNR IRIS | CNR IRIS
2021
Other
Open Access
4SECURail - Technical Informative Note 15 - Progress Report: Formal development Demonstrator Prototype
Mazzanti F, Belli D
This Technical Informative Note describes the progress of the activity of Work Package 2 / Task 2.3 in the months 12-17 of the project 4SECURail. The final results of Task 2.3 will be described in Deliverable 2.5, due at month 20 (end of July 2021). This Technical Informative Note is likely to already contain most of the interesting results that will appear in the final deliverable, together with other less important internal progress details that for readability issues will not appear in the final version. The overall final purpose of the whole experimentation is the observation of the impact, in our specific case, i.e. applying our specific tools and methodologies1 to our specific case study2, of the adoption of formal methods towards the improvement of the quality of the system specifications under construction.Project(s): 4SECURAIL
Mazzanti F, Belli D
This Technical Informative Note describes the progress of the activity of Work Package 2 / Task 2.3 in the months 12-17 of the project 4SECURail. The final results of Task 2.3 will be described in Deliverable 2.5, due at month 20 (end of July 2021). This Technical Informative Note is likely to already contain most of the interesting results that will appear in the final deliverable, together with other less important internal progress details that for readability issues will not appear in the final version. The overall final purpose of the whole experimentation is the observation of the impact, in our specific case, i.e. applying our specific tools and methodologies1 to our specific case study2, of the adoption of formal methods towards the improvement of the quality of the system specifications under construction.Project(s): 4SECURAIL
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2021
Other
Open Access
Systematic evaluation and usability analysis of formal tools for railway system design
Ferrari A, Mazzanti F, Basile D, Ter Beek Mh
Formal methods and supporting tools have a long record of success in the development of safety-critical systems. However, no single tool has emerged as the dominant solution for system design. Each tool differs from the others in terms of the modeling language used, its verification capabilities and other complementary features, and each development context has peculiar needs that require different tools. This is particularly problematic for the railway industry, in which formal methods are highly recommended by the norms, but no actual guidance is provided for the selection of tools. To guide companies in the selection of the most appropriate formal tools to adopt in their contexts, a clear assessment of the features of the currently available tools is required. To address this goal, this paper considers a set of 13 formal tools that have been used for railway system design, and it presents a systematic evaluation of such tools and a preliminary usability analysis of a subset of 7 tools, involving railway practitioners. The results are discussed considering the most desired aspects by industry and earlier related studies. While the focus is on the railway domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal tools and it shows that despite the poor graphical interfaces, usability and maturity of the tools are not major problems, as claimed by contributions from the literature. Instead, support for process integration is the most relevant obstacle for the adoption of most of the tools.DOI: https://doi.org/10.32079/isti-tr-2021/007
DOI: 10.32079/isti-tr-2021/007
Project(s): 4SECURAIL, ASTRail
Metrics:
Ferrari A, Mazzanti F, Basile D, Ter Beek Mh
Formal methods and supporting tools have a long record of success in the development of safety-critical systems. However, no single tool has emerged as the dominant solution for system design. Each tool differs from the others in terms of the modeling language used, its verification capabilities and other complementary features, and each development context has peculiar needs that require different tools. This is particularly problematic for the railway industry, in which formal methods are highly recommended by the norms, but no actual guidance is provided for the selection of tools. To guide companies in the selection of the most appropriate formal tools to adopt in their contexts, a clear assessment of the features of the currently available tools is required. To address this goal, this paper considers a set of 13 formal tools that have been used for railway system design, and it presents a systematic evaluation of such tools and a preliminary usability analysis of a subset of 7 tools, involving railway practitioners. The results are discussed considering the most desired aspects by industry and earlier related studies. While the focus is on the railway domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal tools and it shows that despite the poor graphical interfaces, usability and maturity of the tools are not major problems, as claimed by contributions from the literature. Instead, support for process integration is the most relevant obstacle for the adoption of most of the tools.DOI: https://doi.org/10.32079/isti-tr-2021/007
DOI: 10.32079/isti-tr-2021/007
Project(s): 4SECURAIL
, ASTRail Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2021
Conference article
Open Access
Static analysis and family-based model checking of featured transition systems with VMC
Ter Beek Mh, Mazzanti F, Damiani F, Paolini L, Scarso G, Valfrè M, Lienhardt M
A Featured Transition System (FTS) is a formalism for modeling variability in configurable system behavior. The behavior of all variants (products) is modeled in a single compact FTS by associating the possibility to perform an action and transition from one state to another with feature expressions that condition the execution of an action in specific variants. We present a front-end for the research tool VMC. The resulting toolchain allows a modeler to analyze an FTS for ambiguities (dead or false optional transitions and hidden deadlock states), transform an ambiguous FTS into an unambiguous one, and perform an efficient kind of family-based verification of an FTS without hidden deadlock states. We use benchmarks from the literature to demonstrate the novelties offered by the toolchain.DOI: 10.1145/3461002.3473071
Metrics:
Ter Beek Mh, Mazzanti F, Damiani F, Paolini L, Scarso G, Valfrè M, Lienhardt M
A Featured Transition System (FTS) is a formalism for modeling variability in configurable system behavior. The behavior of all variants (products) is modeled in a single compact FTS by associating the possibility to perform an action and transition from one state to another with feature expressions that condition the execution of an action in specific variants. We present a front-end for the research tool VMC. The resulting toolchain allows a modeler to analyze an FTS for ambiguities (dead or false optional transitions and hidden deadlock states), transform an ambiguous FTS into an unambiguous one, and perform an efficient kind of family-based verification of an FTS without hidden deadlock states. We use benchmarks from the literature to demonstrate the novelties offered by the toolchain.DOI: 10.1145/3461002.3473071
Metrics:
See at:
dl.acm.org | CNR IRIS | ISTI Repository | CNR IRIS | CNR IRIS
2021
Conference article
Open Access
Static analysis and family-based model checking with VMC
Ter Beek Mh, Mazzanti F, Damiani F, Paolini L, Scarso G, Lienhardt M
VMC is a research tool for model checking variability-rich behavioural models specified as a modal transition system (MTS) with variability constraints (MTSv). In this tutorial, we introduce a tool chain built on VMC that allows to perform an efficient kind of family-based model checking in absence of deadlocks. It accepts as input either an MTSv or a featured transition system (FTS).DOI: 10.1145/3461001.3472732
Metrics:
Ter Beek Mh, Mazzanti F, Damiani F, Paolini L, Scarso G, Lienhardt M
VMC is a research tool for model checking variability-rich behavioural models specified as a modal transition system (MTS) with variability constraints (MTSv). In this tutorial, we introduce a tool chain built on VMC that allows to perform an efficient kind of family-based model checking in absence of deadlocks. It accepts as input either an MTSv or a featured transition system (FTS).DOI: 10.1145/3461001.3472732
Metrics:
See at:
dl.acm.org | CNR IRIS | ISTI Repository | ISTI Repository | CNR IRIS | CNR IRIS | CNR IRIS
2021
Other
Open Access
4SECURail - Revised requirements of the 4SECURail case study
Mazzanti F, Belli D
The final version of the system requirements of the case study used in the 4SECURail demonstratorDOI: http://doi.org/10.5281/zenodo.5541217
DOI: 10.5281/zenodo.5541217
Project(s): 4SECURAIL
Metrics:
Mazzanti F, Belli D
The final version of the system requirements of the case study used in the 4SECURail demonstratorDOI: http://doi.org/10.5281/zenodo.5541217
DOI: 10.5281/zenodo.5541217
Project(s): 4SECURAIL
Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2021
Software
Open Access
Formal models of the SAI/CSL system of the 4SECURail case study
Mazzanti F, Belli D
Formal models of 4SECURAIL case study in the notation accepted by UMC, ProB, CADP/LNTDOI: http://doi.org/10.5281/zenodo.5541307
DOI: 10.5281/zenodo.5541307
Project(s): 4SECURAIL
Metrics:
Mazzanti F, Belli D
Formal models of 4SECURAIL case study in the notation accepted by UMC, ProB, CADP/LNTDOI: http://doi.org/10.5281/zenodo.5541307
DOI: 10.5281/zenodo.5541307
Project(s): 4SECURAIL
Metrics: