2022
Journal article
Open Access
Efficient static analysis and verification of featured transition systems
Ter Beek M. H., 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 (Online) 27 (2022). doi:10.1007/s10664-020-09930-8
DOI: 10.1007/s10664-020-09930-8
Metrics:
Ter Beek M. H., 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 (Online) 27 (2022). doi:10.1007/s10664-020-09930-8
DOI: 10.1007/s10664-020-09930-8
Metrics:
See at:
link.springer.com 
| ISTI Repository | ISTI Repository | CNR ExploRA
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: MARS 2022 - Fifth Workshop on Models for Formal Analysis of Real Systems, 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: MARS 2022 - Fifth Workshop on Models for Formal Analysis of Real Systems, 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 | ISTI Repository | CNR ExploRA
2022
Journal article
Open Access
FTS4VMC: a front-end tool for static analysis and family-based model checking of FTSs with VMC
Ter Beek M. H., 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 (Print) 224 (2022). doi:10.1016/j.scico.2022.102879
DOI: 10.1016/j.scico.2022.102879
Metrics:
Ter Beek M. H., 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 (Print) 224 (2022). doi:10.1016/j.scico.2022.102879
DOI: 10.1016/j.scico.2022.102879
Metrics:
See at:
ISTI Repository | CNR ExploRA 
| www.sciencedirect.com
2022
Conference article
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.Source: F-IDE 2022 - 7th Workshop on Formal Integrated Development Environment, Berlin, Germany, 26/09/2022
Project(s): 4SECURAIL
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.Source: F-IDE 2022 - 7th Workshop on Formal Integrated Development Environment, Berlin, Germany, 26/09/2022
Project(s): 4SECURAIL
See at:
ISTI Repository | CNR ExploRA
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.Source: RSSRail 2022 - 4th International Conference on Reliability, Safety, and Security of Railway Systems, pp. 149–165, Paris, France, 1-2/06/2022
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.Source: RSSRail 2022 - 4th International Conference on Reliability, Safety, and Security of Railway Systems, pp. 149–165, Paris, France, 1-2/06/2022
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 | ISTI Repository | doi.org | link.springer.com | CNR ExploRA
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: Transport Research Arena (TRA) Conference, 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: Transport Research Arena (TRA) Conference, Lisbon, Portugal, 13-14/11/2022
Project(s): 4SECURAIL
See at:
ISTI Repository | CNR ExploRA
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) (2021). doi:10.1007/s10703-021-00360-w
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) (2021). doi:10.1007/s10703-021-00360-w
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 | ISTI Repository | doi.org | Formal Methods in System Design | INRIA a CCSD electronic archive server | HAL Descartes | link.springer.com | CNR ExploRA
2021
Report
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.Source: Project report, 4SECURail, TIN-FM-15, pp.1–53, 2021
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.Source: Project report, 4SECURail, TIN-FM-15, pp.1–53, 2021
Project(s): 4SECURAIL
See at:
ISTI Repository | CNR ExploRA
2021
Report
Open Access
Systematic evaluation and usability analysis of formal tools for railway system design
Ferrari A., Mazzanti F., Basile D., Ter Beek M. H.
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.Source: ISTI-2021-TR/007, 2021
DOI: 10.32079/isti-tr-2021/007
Project(s): 4SECURAIL, ASTRail
Metrics:
Ferrari A., Mazzanti F., Basile D., Ter Beek M. H.
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.Source: ISTI-2021-TR/007, 2021
DOI: 10.32079/isti-tr-2021/007
Project(s): 4SECURAIL
, ASTRail Metrics:
See at:
CNR ExploRA
2021
Conference article
Open Access
Static analysis and family-based model checking of featured transition systems with VMC
Ter Beek M. H., 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.Source: SPLC'21 - 25th ACM International Systems and Software Product Line Conference, pp. 24–27, Leicester, UK, 06-10/09/2021
DOI: 10.1145/3461002.3473071
Metrics:
Ter Beek M. H., 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.Source: SPLC'21 - 25th ACM International Systems and Software Product Line Conference, pp. 24–27, Leicester, UK, 06-10/09/2021
DOI: 10.1145/3461002.3473071
Metrics:
See at:
ISTI Repository | dl.acm.org | CNR ExploRA
2021
Conference article
Open Access
Static analysis and family-based model checking with VMC
Ter Beek M. H., 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).Source: SPLC'21 - 25th International Systems and Software Product Line Conference, pp. 214–214, Leicester, UK, 06-10/09/2021
DOI: 10.1145/3461001.3472732
Metrics:
Ter Beek M. H., 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).Source: SPLC'21 - 25th International Systems and Software Product Line Conference, pp. 214–214, Leicester, UK, 06-10/09/2021
DOI: 10.1145/3461001.3472732
Metrics:
See at:
ISTI Repository | ISTI Repository | dl.acm.org | CNR ExploRA
2021
Report
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 demonstratorSource: ISTI Project report, 4SECURail, 2021
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 demonstratorSource: ISTI Project report, 4SECURail, 2021
DOI: 10.5281/zenodo.5541217
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository | CNR ExploRA
2021
Software
Unknown
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: 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: 10.5281/zenodo.5541307
Project(s): 4SECURAIL
Metrics:
See at: CNR ExploRA
2021
Software
Unknown
The UMC2LNT and UMC2PROB model transformation tools
Mazzanti F., Belli D.
This documents contains the source code of two trasformation tools used in the 4SECURail project. The tools umc2lnt takes as argument the name of a file contining an UMC model and generates the corresponding CADP/LNT model.DOI: 10.5281/zenodo.5541350
Project(s): 4SECURAIL
Metrics:
Mazzanti F., Belli D.
This documents contains the source code of two trasformation tools used in the 4SECURail project. The tools umc2lnt takes as argument the name of a file contining an UMC model and generates the corresponding CADP/LNT model.DOI: 10.5281/zenodo.5541350
Project(s): 4SECURAIL
Metrics:
See at: CNR ExploRA
2021
Report
Open Access
4SECURail - Formal development demonstrator prototype, final release
Mazzanti F., Belli D.
This Deliverable describes the final results of Task 2.3 of 4SECURail project. The goal of Task 2.3 is to apply the formal development demonstrator process defined in Task 2.1 to the signalling case study defined in Task 2.2 and to describe the observed impact of the selected tools and methodologies for improving the quality of the system specifications under analysis.Source: ISTI Project report, 4SECURail, 2021
Project(s): 4SECURAIL
Mazzanti F., Belli D.
This Deliverable describes the final results of Task 2.3 of 4SECURail project. The goal of Task 2.3 is to apply the formal development demonstrator process defined in Task 2.1 to the signalling case study defined in Task 2.2 and to describe the observed impact of the selected tools and methodologies for improving the quality of the system specifications under analysis.Source: ISTI Project report, 4SECURail, 2021
Project(s): 4SECURAIL
See at:
ISTI Repository | CNR ExploRA
2021
Journal article
Open Access
Systematic evaluation and usability analysis of formal methods tools for railway signaling system design
Ferrari A., Mazzanti F., Basile D., Ter Beek M. H.
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 methods 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 methods tools that have been used for the early design of railway systems, 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 signaling domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal methods 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. Our contribution can be useful to R&D engineers from railway signaling companies and infrastructure managers, but also to tool developers and academic researchers alike.Source: IEEE transactions on software engineering 48 (2021): 4675–4691. doi:10.1109/TSE.2021.3124677
DOI: 10.1109/tse.2021.3124677
Project(s): 4SECURAIL, ASTRail
Metrics:
Ferrari A., Mazzanti F., Basile D., Ter Beek M. H.
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 methods 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 methods tools that have been used for the early design of railway systems, 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 signaling domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal methods 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. Our contribution can be useful to R&D engineers from railway signaling companies and infrastructure managers, but also to tool developers and academic researchers alike.Source: IEEE transactions on software engineering 48 (2021): 4675–4691. doi:10.1109/TSE.2021.3124677
DOI: 10.1109/tse.2021.3124677
Project(s): 4SECURAIL
, ASTRail Metrics:
See at:
ISTI Repository | ieeexplore.ieee.org | CNR ExploRA
2020
Conference article
Open Access
Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
Lang F., Mateescu R., Mazzanti F.
We showed in a recent paper that, when verifying a modal?-calculus formula, the actions of the system under verification can bepartitioned into sets of so-called weak and strong actions, depending onthe combination of weak and strong modalities occurring in the formula.In a compositional verification setting, where the system consists of pro-cesses executing in parallel, this partition allows us to decide whethereach individual process can be minimized for either divergence-preservingbranching (if the process contains only weak actions) or strong (other-wise) bisimilarity, while preserving the truth value of the formula. In thispaper, we refine this idea by devising a family of bisimilarity relations,named sharp bisimilarities, parameterized by the set of strong actions.We show that these relations have all the nice properties necessary tobe used for compositional verification, in particular congruence and ad-equacy with the logic. We also illustrate their practical utility on severalexamples and case-studies, and report about our success in the RERS2019 model checking challenge.Source: 26th International Conference, TACAS 2020, pp. 57–73, Dublin, Ireland, April 25-30, 2020
DOI: 10.1007/978-3-030-45237-7_4
Metrics:
Lang F., Mateescu R., Mazzanti F.
We showed in a recent paper that, when verifying a modal?-calculus formula, the actions of the system under verification can bepartitioned into sets of so-called weak and strong actions, depending onthe combination of weak and strong modalities occurring in the formula.In a compositional verification setting, where the system consists of pro-cesses executing in parallel, this partition allows us to decide whethereach individual process can be minimized for either divergence-preservingbranching (if the process contains only weak actions) or strong (other-wise) bisimilarity, while preserving the truth value of the formula. In thispaper, we refine this idea by devising a family of bisimilarity relations,named sharp bisimilarities, parameterized by the set of strong actions.We show that these relations have all the nice properties necessary tobe used for compositional verification, in particular congruence and ad-equacy with the logic. We also illustrate their practical utility on severalexamples and case-studies, and report about our success in the RERS2019 model checking challenge.Source: 26th International Conference, TACAS 2020, pp. 57–73, Dublin, Ireland, April 25-30, 2020
DOI: 10.1007/978-3-030-45237-7_4
Metrics:
See at:
doi.org | Europe PubMed Central | link.springer.com | link.springer.com | ISTI Repository | CNR ExploRA | INRIA a CCSD electronic archive server
2020
Journal article
Open Access
A Formal Methods Demonstrator for Railways
Mazzanti F., Basile D.
The 4SECURail project - funded by the European UnionHorizon 2020 Shift2Rail Joint Undertaking - has twooverall objectives: to design a Computer Security IncidentResponse Team (CSIRT) for joint EU-Rail cybersecurity,and the setup of a Formal Methods Demonstrator for theevaluation, in terms of cost, benefits and requiredlearning curve, of the impact of the use of FormalMethods for the rigorous specification of thecomponents of a railway signalling infrastructure.Source: ERCIM news online edition 121 (2020).
Mazzanti F., Basile D.
The 4SECURail project - funded by the European UnionHorizon 2020 Shift2Rail Joint Undertaking - has twooverall objectives: to design a Computer Security IncidentResponse Team (CSIRT) for joint EU-Rail cybersecurity,and the setup of a Formal Methods Demonstrator for theevaluation, in terms of cost, benefits and requiredlearning curve, of the impact of the use of FormalMethods for the rigorous specification of thecomponents of a railway signalling infrastructure.Source: ERCIM news online edition 121 (2020).
See at:
ercim-news.ercim.eu | ISTI Repository | CNR ExploRA
2020
Conference article
Open Access
Comparing formal tools for system design: a judgment study
Ferrari A, Mazzantif., Basile D., Ter Beek M. H., Fantechi A.
Formal methods and tools have a long history of successful applications in the design of safety-critical railway products. However, most of the experiences focused on the application of a single method at once, and little work has been performed to compare the applicability of the different available frameworks to the railway context. As a result, companies willing to introduce formal methods in their development process have little guidance on the selection of tools that couldfi t their needs. To address this goal, this paper presents a comparison between 9 different formal tools, namely Atelier B, CADP, FDR4, NuSMV, ProB, Simulink, SPIN, UMC, and UPPAAL SMC. We performed a judgment study, involving 17 experts with experience in formal methods applied to railways. In the study, part of the experts were required to model a railway signaling problem (a moving-block train distancing system) with the different tools, and to provide feedback on their experience. The information produced was then synthesized, and the results were validated by the remaining experts. Based on the outcome of this process, we provide a synthesis that describes when to use a certain tool, and what are the problems that may be faced by modelers. Our experience shows that the different tools serve different purposes, and multiple formal methods are required to fully cover the needs of the railway system design process.Source: ICSE'20 - 42nd International Conference on Software Engineering, pp. 62–74, Seoul, Republic of Korea, 27/6/2020-19/7/2020
DOI: 10.1145/3377811.3380373
Project(s): 4SECURAIL, ASTRail
Metrics:
Ferrari A, Mazzantif., Basile D., Ter Beek M. H., Fantechi A.
Formal methods and tools have a long history of successful applications in the design of safety-critical railway products. However, most of the experiences focused on the application of a single method at once, and little work has been performed to compare the applicability of the different available frameworks to the railway context. As a result, companies willing to introduce formal methods in their development process have little guidance on the selection of tools that couldfi t their needs. To address this goal, this paper presents a comparison between 9 different formal tools, namely Atelier B, CADP, FDR4, NuSMV, ProB, Simulink, SPIN, UMC, and UPPAAL SMC. We performed a judgment study, involving 17 experts with experience in formal methods applied to railways. In the study, part of the experts were required to model a railway signaling problem (a moving-block train distancing system) with the different tools, and to provide feedback on their experience. The information produced was then synthesized, and the results were validated by the remaining experts. Based on the outcome of this process, we provide a synthesis that describes when to use a certain tool, and what are the problems that may be faced by modelers. Our experience shows that the different tools serve different purposes, and multiple formal methods are required to fully cover the needs of the railway system design process.Source: ICSE'20 - 42nd International Conference on Software Engineering, pp. 62–74, Seoul, Republic of Korea, 27/6/2020-19/7/2020
DOI: 10.1145/3377811.3380373
Project(s): 4SECURAIL
, ASTRail Metrics:
See at:
ISTI Repository | 2020.icse-conferences.org | doi.org | CNR ExploRA
2020
Conference article
Open Access
Designing a demonstrator of formal methods for railways infrastructure managers
Basile D., Ter Beek M. H., Fantechi A., Ferrari A., Gnesi S., Masullo L., Mazzanti F., Piattino A., Trentini D.
The Shift2Rail Innovation Programme (IP) is focussing on innovative technologies to enhance the overall railway market segments. Formal methods and standard interfaces have been identified as two key concepts to reduce time-to-market and costs, while ensuring safety, interoperability and standardisation. However, the decision to start using formal methods is still deemed too risky. Demonstrating technical and commercial benefits of both formal methods and standard interfaces is necessary to address the obstacles of learning curve and lack of clear cost/benefit analysis that are hindering their adoption, and this is the goal of the 4SECURail project, recently funded by the Shift2Rail IP. In this paper, we provide the reasoning and the rationale for designing the formal methods demonstrator for the 4SECURail project. The design concerns two important issues that have been analysed: (i) the usefulness of formal methods from the point of view of the infrastructure managers, (ii) the adoption of a semi-formal SysML notation within our formal methods demonstrator process.Source: ISoLA'20 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Applications, pp. 467–485, Rhodes, Greece, 20-30 October, 2020
DOI: 10.1007/978-3-030-61467-6_30
Project(s): 4SECURAIL
Metrics:
Basile D., Ter Beek M. H., Fantechi A., Ferrari A., Gnesi S., Masullo L., Mazzanti F., Piattino A., Trentini D.
The Shift2Rail Innovation Programme (IP) is focussing on innovative technologies to enhance the overall railway market segments. Formal methods and standard interfaces have been identified as two key concepts to reduce time-to-market and costs, while ensuring safety, interoperability and standardisation. However, the decision to start using formal methods is still deemed too risky. Demonstrating technical and commercial benefits of both formal methods and standard interfaces is necessary to address the obstacles of learning curve and lack of clear cost/benefit analysis that are hindering their adoption, and this is the goal of the 4SECURail project, recently funded by the Shift2Rail IP. In this paper, we provide the reasoning and the rationale for designing the formal methods demonstrator for the 4SECURail project. The design concerns two important issues that have been analysed: (i) the usefulness of formal methods from the point of view of the infrastructure managers, (ii) the adoption of a semi-formal SysML notation within our formal methods demonstrator process.Source: ISoLA'20 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Applications, pp. 467–485, Rhodes, Greece, 20-30 October, 2020
DOI: 10.1007/978-3-030-61467-6_30
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository | ISTI Repository | link.springer.com | link.springer.com | CNR ExploRA