2026
Journal article
Open Access
A history of formal methods in railways
Ter Beek Maurice, Fantechi Alessandro, Ferrari Alessio, Gnesi Stefania, Haxthausen Anne E., Lecomte Thierry
The engineering of industrial systems, particularly in safety-critical domains such as railways, demands rigorous verification and validation processes to ensure system dependability. Formal methods have emerged as powerful tools to complement traditional software engineering practices. In the railway sector, which increasingly relies on complex, distributed, and cyber-physical control systems, formal methods have demonstrated particular value for many decades now. In this paper, we provide a retrospective overview of the application of formal methods and tools in the railway domain, with emphasis on two prominent verification approaches and one frequently verified railway system: modeling and validation with the B method and tools and formal verification of interlocking systems by model checking. We explore their role in the design and development of key railway systems, highlighting both academic research and industrial success stories, as witnessed by international projects and initiatives. We conclude with an outlook on the potential of integrating AI and formal methods to enhance the efficiency of next-generation railway systems.Source: FORMAL ASPECTS OF COMPUTING, vol. 38 (issue 3), pp. 27:1-27:38
DOI: 10.1145/3802545
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Ter Beek Maurice, Fantechi Alessandro, Ferrari Alessio, Gnesi Stefania, Haxthausen Anne E., Lecomte Thierry
The engineering of industrial systems, particularly in safety-critical domains such as railways, demands rigorous verification and validation processes to ensure system dependability. Formal methods have emerged as powerful tools to complement traditional software engineering practices. In the railway sector, which increasingly relies on complex, distributed, and cyber-physical control systems, formal methods have demonstrated particular value for many decades now. In this paper, we provide a retrospective overview of the application of formal methods and tools in the railway domain, with emphasis on two prominent verification approaches and one frequently verified railway system: modeling and validation with the B method and tools and formal verification of interlocking systems by model checking. We explore their role in the design and development of key railway systems, highlighting both academic research and industrial success stories, as witnessed by international projects and initiatives. We conclude with an outlook on the potential of integrating AI and formal methods to enhance the efficiency of next-generation railway systems.Source: FORMAL ASPECTS OF COMPUTING, vol. 38 (issue 3), pp. 27:1-27:38
DOI: 10.1145/3802545
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
dl.acm.org 
| CNR IRIS | CNR IRIS 
| CNR IRIS
2025
Conference article
Restricted
Combining established and emerging techniques to detect inconsistencies in requirements
Fantechi A., Gnesi S., Semini L.
Previous work has investigated the adequacy of LLMs to detect inconsistencies in requirements documents, but has also shown their limitations with real case studies. In this paper, we propose a hybrid approach, which exploits traditional clustering techniques to help LLMs focus on potential inconsistencies. The approach was evaluated using a large security requirements document from the RE Open Data Initiative, with injected inconsistencies. Results show that combining LLM-based detection with rule-based clustering enhances both precision and recall.DOI: 10.1109/re63999.2025.00062
Metrics:
Fantechi A., Gnesi S., Semini L.
Previous work has investigated the adequacy of LLMs to detect inconsistencies in requirements documents, but has also shown their limitations with real case studies. In this paper, we propose a hybrid approach, which exploits traditional clustering techniques to help LLMs focus on potential inconsistencies. The approach was evaluated using a large security requirements document from the RE Open Data Initiative, with injected inconsistencies. Results show that combining LLM-based detection with rule-based clustering enhances both precision and recall.DOI: 10.1109/re63999.2025.00062
Metrics:
See at:
doi.org | CNR IRIS | ieeexplore.ieee.org | CNR IRIS
2025
Conference article
Open Access
Quantitative dependability evaluation of train control systems in presence of uncertainty: a systematic literature review
Carnevali Laura, Di Giandomenico Felicita, Fantechi Alessandro, Gnesi Stefania, Gori Gloria
Technological advances in Train Control Systems (TCSs) hold substantial promise for revolutionizing railway transportation de- pendability in terms of safety, availability, and operational capacity. This transformation is primarily driven by cutting-edge distancing policies such as Moving Block (MB) signaling and Virtual Coupling (VC), which are powered by sophisticated train localization technologies including satellite-based positioning systems. At the same time, these technolog- ical advances raise notable concerns about the effects that uncertainty in critical TCS parameters, such as train position and speed, may have on dependability-related attributes. This is an extended abstract of the journal paper [6], where a comprehensive systematic literature review in- vestigating quantitative methodologies for assessing TCS dependability under uncertain conditions is presented. Through selection and analysis of 42 peer-reviewed publications spanning 2011-2023, we provide em- pirical insights and a taxonomic framework on research and practice in quantitative dependability assessment of TCSs.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16236, pp. 129-134. Pisa, Italy, 26–28 November 2025
DOI: 10.1007/978-3-032-10762-6_11
DOI: 10.1109/tits.2025.3530112
Metrics:
Carnevali Laura, Di Giandomenico Felicita, Fantechi Alessandro, Gnesi Stefania, Gori Gloria
Technological advances in Train Control Systems (TCSs) hold substantial promise for revolutionizing railway transportation de- pendability in terms of safety, availability, and operational capacity. This transformation is primarily driven by cutting-edge distancing policies such as Moving Block (MB) signaling and Virtual Coupling (VC), which are powered by sophisticated train localization technologies including satellite-based positioning systems. At the same time, these technolog- ical advances raise notable concerns about the effects that uncertainty in critical TCS parameters, such as train position and speed, may have on dependability-related attributes. This is an extended abstract of the journal paper [6], where a comprehensive systematic literature review in- vestigating quantitative methodologies for assessing TCS dependability under uncertain conditions is presented. Through selection and analysis of 42 peer-reviewed publications spanning 2011-2023, we provide em- pirical insights and a taxonomic framework on research and practice in quantitative dependability assessment of TCSs.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16236, pp. 129-134. Pisa, Italy, 26–28 November 2025
DOI: 10.1007/978-3-032-10762-6_11
DOI: 10.1109/tits.2025.3530112
Metrics:
See at:
IRIS Cnr | IRIS Cnr | IRIS Cnr | doi.org | IEEE Transactions on Intelligent Transportation Systems | CNR IRIS | Flore (Florence Research Repository) | CNR IRIS | CNR IRIS | link.springer.com
2025
Other
Restricted
PRIN PNRR Adventure D2: Report on the definition of methods for qualitative and quantitative evaluation of KPIs of railway systems
Basile D., Ter Beek M., Carnevali L., Chiaradonna S., Di Giandomenico F., Fantechi A., Gori G.
ADVENTURE (ADVancEd iNtegraTed evalUation of Railway systEms) aims at developing innovative solutions for the evaluation of complex railway systems. Using Model-Driven Engineering (MDE) methods and multi-paradigm or multi-formalism approaches to help create bridges between different abstraction levels, the project focuses on the following objectives: 1) qualitative evaluation of safety of complex distributed railway systems, by means of diverse techniques such as compositional model checking, synthesis of specifications given as behavioral interfaces, and tool support for relating specifications with implementations; 2) quantitative evaluation of dependability attributes in spite of failures, in particular considering communication failures, through quantitative modeling and evaluation of the timed failure logic of the system; 3) quantitative evaluation of trade-offs between energy efficiency and availability/performance, considering different smart policies of energy saving and taking into account failures, criticalities, and priorities of the system under analysis. The developed solutions are going to be experimented and validated by their application to different case studies, that are considered as representative of the innovation trends in railways, namely decentralized interlocking systems, standard interfaces and smart deicing systems. This deliverable details the techniques that have been considered and the advancements.Project(s): ADVancEd iNtegraTed evalUation of Railway systEms
Basile D., Ter Beek M., Carnevali L., Chiaradonna S., Di Giandomenico F., Fantechi A., Gori G.
ADVENTURE (ADVancEd iNtegraTed evalUation of Railway systEms) aims at developing innovative solutions for the evaluation of complex railway systems. Using Model-Driven Engineering (MDE) methods and multi-paradigm or multi-formalism approaches to help create bridges between different abstraction levels, the project focuses on the following objectives: 1) qualitative evaluation of safety of complex distributed railway systems, by means of diverse techniques such as compositional model checking, synthesis of specifications given as behavioral interfaces, and tool support for relating specifications with implementations; 2) quantitative evaluation of dependability attributes in spite of failures, in particular considering communication failures, through quantitative modeling and evaluation of the timed failure logic of the system; 3) quantitative evaluation of trade-offs between energy efficiency and availability/performance, considering different smart policies of energy saving and taking into account failures, criticalities, and priorities of the system under analysis. The developed solutions are going to be experimented and validated by their application to different case studies, that are considered as representative of the innovation trends in railways, namely decentralized interlocking systems, standard interfaces and smart deicing systems. This deliverable details the techniques that have been considered and the advancements.Project(s): ADVancEd iNtegraTed evalUation of Railway systEms
2024
Other
Restricted
PRIN PNRR Adventure D1.1 - Report on the definition of the case studies
Basile D., Ter Beek M., Carnevali L., Chiaradonna S., Di Giandomenico F., Fantechi A., Gori G.
ADVENTURE (ADVancEd iNtegraTed evalUation of Railway systEms) aims at developing innovative solutions for the evaluation of complex railway systems. Using Model-Driven Engineering (MDE) methods and multi-paradigm or multi-formalism approaches to help create bridges between different abstraction levels, the project focuses on the following objectives: 1) qualitative evaluation of safety of complex distributed railway systems, by means of diverse techniques such as compositional model checking, synthesis of specifications given as behavioral interfaces, and tool support for relating specifications with implementations; 2) quantitative evaluation of dependability attributes in spite of failures, in particular considering communication failures, through quantitative modeling and evaluation of the timed failure logic of the system; 3) quantitative evaluation of trade-offs between energy efficiency and availability/performance, considering different smart policies of energy saving and taking into account failures, criticalities, and priorities of the system under analysis. The developed solutions are going to be experimented and validated by their application to different case studies, that are considered as representative of the innovation trends in railways, namely decentralized interlocking systems, standard interfaces and smart deicing systems. A common trait of these case studies is that they can be considered as distributed Cyber-Physical Systems that ensure safe transit of trains along a station route. In all cases, the route is allocated if specific conditions are verified on a set of elements lying along the route, with also an eye to the energy consumption in case the involved equipment are characterized by energy-intensive operation. A failure of one of these elements generally means that the itinerary is unavailable: in this case, the availability and thus the overall transit capacity of the station decreases as well, with the possible occurrence of single points of failure blocking all operations. Modeling such a complex system for the purpose of quantitative assessment of availability suffers from the problem of state-space explosion. It is therefore desired to: (a)~identify a model-based compositional method for analyzing such a complex network by combining results of the analysis of its elements, with the aim to perform network analysis in linear time with respect to the number of elements; the approach will be tried on some topological instances of the two case studies; (b)~generalize the identified approach so that it can be automatically instantiated on different network topologies, both for ADVENTURE case studies and for networks defining other distributed systems that have similar characteristics or similar dependability requirements.Project(s): ADVancEd iNtegraTed evalUation of Railway systEms
Basile D., Ter Beek M., Carnevali L., Chiaradonna S., Di Giandomenico F., Fantechi A., Gori G.
ADVENTURE (ADVancEd iNtegraTed evalUation of Railway systEms) aims at developing innovative solutions for the evaluation of complex railway systems. Using Model-Driven Engineering (MDE) methods and multi-paradigm or multi-formalism approaches to help create bridges between different abstraction levels, the project focuses on the following objectives: 1) qualitative evaluation of safety of complex distributed railway systems, by means of diverse techniques such as compositional model checking, synthesis of specifications given as behavioral interfaces, and tool support for relating specifications with implementations; 2) quantitative evaluation of dependability attributes in spite of failures, in particular considering communication failures, through quantitative modeling and evaluation of the timed failure logic of the system; 3) quantitative evaluation of trade-offs between energy efficiency and availability/performance, considering different smart policies of energy saving and taking into account failures, criticalities, and priorities of the system under analysis. The developed solutions are going to be experimented and validated by their application to different case studies, that are considered as representative of the innovation trends in railways, namely decentralized interlocking systems, standard interfaces and smart deicing systems. A common trait of these case studies is that they can be considered as distributed Cyber-Physical Systems that ensure safe transit of trains along a station route. In all cases, the route is allocated if specific conditions are verified on a set of elements lying along the route, with also an eye to the energy consumption in case the involved equipment are characterized by energy-intensive operation. A failure of one of these elements generally means that the itinerary is unavailable: in this case, the availability and thus the overall transit capacity of the station decreases as well, with the possible occurrence of single points of failure blocking all operations. Modeling such a complex system for the purpose of quantitative assessment of availability suffers from the problem of state-space explosion. It is therefore desired to: (a)~identify a model-based compositional method for analyzing such a complex network by combining results of the analysis of its elements, with the aim to perform network analysis in linear time with respect to the number of elements; the approach will be tried on some topological instances of the two case studies; (b)~generalize the identified approach so that it can be automatically instantiated on different network topologies, both for ADVENTURE case studies and for networks defining other distributed systems that have similar characteristics or similar dependability requirements.Project(s): ADVancEd iNtegraTed evalUation of Railway systEms
2024
Conference article
Open Access
An integrated perspective on the evaluation of complex railway systems
Basile D., Ter Beek M. H., Carnevali L., Chiaradonna S., Di Giandomenico F., Fantechi A., Gori G.
The project ADVENTURE (ADVancEd iNtegraTed evalUation of Railway systEms) aims to provide novel solutions for the evaluation of RAMS requirements as well as to present trade-offs between dependability attributes and energy consumption in complex railway systems, leveraging both qualitative and quantitative evaluation methods. To this end, case studies concerning distributed interlocking systems, standard interfaces, and railroad switch heaters are considered, comprising different challenging scenarios, notably representative of the complexity of railway systems. In this paper, we illustrate the objectives of the project and the activities planned to address them, devising future steps to integrate the envisaged contributions within a unified framework.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15223, pp. 190-207. Crete, Greece, 27-31/10/2024
DOI: 10.1007/978-3-031-75390-9_13
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Basile D., Ter Beek M. H., Carnevali L., Chiaradonna S., Di Giandomenico F., Fantechi A., Gori G.
The project ADVENTURE (ADVancEd iNtegraTed evalUation of Railway systEms) aims to provide novel solutions for the evaluation of RAMS requirements as well as to present trade-offs between dependability attributes and energy consumption in complex railway systems, leveraging both qualitative and quantitative evaluation methods. To this end, case studies concerning distributed interlocking systems, standard interfaces, and railroad switch heaters are considered, comprising different challenging scenarios, notably representative of the complexity of railway systems. In this paper, we illustrate the objectives of the project and the activities planned to address them, devising future steps to integrate the envisaged contributions within a unified framework.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15223, pp. 190-207. Crete, Greece, 27-31/10/2024
DOI: 10.1007/978-3-031-75390-9_13
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
IRIS Cnr | IRIS Cnr | IRIS Cnr | Flore (Florence Research Repository) | Flore (Florence Research Repository) | CNR IRIS | CNR IRIS
2024
Conference article
Restricted
Exploring LLMs’ ability to detect variability in requirements
Fantechi A., Gnesi S., Semini L.
In this paper, we address the question of whether general-purpose LLM-based tools may be useful for detecting requirements variability in Natural Language (NL) requirements documents. For this purpose, we conduct a preliminary exploratory study considering OpenAI chatGPT-3.5 and Microsoft Bing. Using two exemplar NL requirements documents, we compare the variability detection capability of the chatbots with that of experts and that of a rule-based NLP tool.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14588, pp. 178-188. Winterthur, Switzerland, 8-11/04/2024
DOI: 10.1007/978-3-031-57327-9_11
Project(s): STENDHAL
Metrics:
Fantechi A., Gnesi S., Semini L.
In this paper, we address the question of whether general-purpose LLM-based tools may be useful for detecting requirements variability in Natural Language (NL) requirements documents. For this purpose, we conduct a preliminary exploratory study considering OpenAI chatGPT-3.5 and Microsoft Bing. Using two exemplar NL requirements documents, we compare the variability detection capability of the chatbots with that of experts and that of a rule-based NLP tool.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14588, pp. 178-188. Winterthur, Switzerland, 8-11/04/2024
DOI: 10.1007/978-3-031-57327-9_11
Project(s): STENDHAL
Metrics:
2024
Journal article
Open Access
Evaluating the understandability and user acceptance of Attack-Defense Trees: original experiment and replication
Broccia G., Ter Beek M. H., Lluch Lafuente A., Spoletini P., Fantechi A., Ferrari A.
Context: Attack-Defense Trees (ADTs) are a graphical notation used to model and evaluate security requirements. ADTs are popular because they facilitate communication among different stakeholders involved in system security evaluation and are formal enough to be verified using methods like model checking. The understandability and user-friendliness of ADTs are claimed as key factors in their success, but these aspects, along with user acceptance, have not been evaluated empirically. Objectives: This paper presents an experiment with 25 subjects designed to assess the understandability and user acceptance of the ADT notation, along with an internal replication involving 49 subjects. Methods: The experiments adapt the Method Evaluation Model (MEM) to examine understandability variables (i.e., effectiveness and efficiency in using ADTs) and user acceptance variables (i.e., ease of use, usefulness, and intention to use). The MEM is also used to evaluate the relationships between these dimensions. In addition, a comparative analysis of the results of the two experiments is carried out. Results: With some minor differences, the outcomes of the two experiments are aligned. The results demonstrate that ADTs are well understood by participants, with values of understandability variables significantly above established thresholds. They are also highly appreciated, particularly for their ease of use. The results also show that users who are more effective in using the notation tend to evaluate it better in terms of usefulness. Conclusion: These studies provide empirical evidence supporting both the understandability and perceived acceptance of ADTs, thus encouraging further adoption of the notation in industrial contexts, and development of supporting tools.Source: INFORMATION AND SOFTWARE TECHNOLOGY, vol. 178
DOI: 10.1016/j.infsof.2024.107624
Project(s): CODECS
, Secure Internet of Things – Risk analysis in design and operation, Security-by-Design in Digital Denmark, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Broccia G., Ter Beek M. H., Lluch Lafuente A., Spoletini P., Fantechi A., Ferrari A.
Context: Attack-Defense Trees (ADTs) are a graphical notation used to model and evaluate security requirements. ADTs are popular because they facilitate communication among different stakeholders involved in system security evaluation and are formal enough to be verified using methods like model checking. The understandability and user-friendliness of ADTs are claimed as key factors in their success, but these aspects, along with user acceptance, have not been evaluated empirically. Objectives: This paper presents an experiment with 25 subjects designed to assess the understandability and user acceptance of the ADT notation, along with an internal replication involving 49 subjects. Methods: The experiments adapt the Method Evaluation Model (MEM) to examine understandability variables (i.e., effectiveness and efficiency in using ADTs) and user acceptance variables (i.e., ease of use, usefulness, and intention to use). The MEM is also used to evaluate the relationships between these dimensions. In addition, a comparative analysis of the results of the two experiments is carried out. Results: With some minor differences, the outcomes of the two experiments are aligned. The results demonstrate that ADTs are well understood by participants, with values of understandability variables significantly above established thresholds. They are also highly appreciated, particularly for their ease of use. The results also show that users who are more effective in using the notation tend to evaluate it better in terms of usefulness. Conclusion: These studies provide empirical evidence supporting both the understandability and perceived acceptance of ADTs, thus encouraging further adoption of the notation in industrial contexts, and development of supporting tools.Source: INFORMATION AND SOFTWARE TECHNOLOGY, vol. 178
DOI: 10.1016/j.infsof.2024.107624
Project(s): CODECS
, Secure Internet of Things – Risk analysis in design and operation, Security-by-Design in Digital Denmark, Typeful Language Adaptation for Dynamic, Interacting and Evolving SystemsMetrics:
See at:
Information and Software Technology | IRIS Cnr | IRIS Cnr | CNR IRIS
2024
Conference article
Open Access
Can AI help with the formalization of railway cybersecurity requirements?
Ter Beek M. H., Fantechi A., Gnesi S., Lenzini G., Petrocchi M.
Driven by and dependent on ICT, like almost everything today, railway transportation has become a critical infrastructure and, as such, is exposed to threats against communication of on-board and wayside components. The shift to cybersecurity brings up the need to comply with new security requirements, and once more security software engineers are confronted with a well-known problem: how to express informal requirements into unambiguous formal expressions that can be translated into enforceable policies or be used to verify the security of a system design. We have experience in translating natural language requirements from standards, regulations, and guidelines into Controlled Natural Language for Data Sharing Agreements (CNL4DSA), a formalism that serves the purpose of bridging natural and formal expressions. The translation of requirements is challenging, calling for a rigorous process of coding agreement between researchers. Following the trend of the time, in this paper, we question whether AI and, in particular, the novel Generative Language Models, can help us with this translation exercise. Previous work shows that AI can help in writing security code, although not always producing secure code; less studied is the quality of generative AI’s working with controlled natural languages in writing requirements for security compliance. Can AI be a valuable tool or companion in this endeavour too? To answer this question, we engage ChatGPT and Microsoft 365 Copilot with the same challenges that we faced when translating cybersecurity requirements for railway systems into CNL4DSA. Comparing our results from some time ago with those of the machine, we found surprising insights, showing the high potentiality of using AI in requirements engineering.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15219, pp. 186-203. Crete, Greece, 27-31/10/2024
DOI: 10.1007/978-3-031-73709-1_12
Metrics:
Ter Beek M. H., Fantechi A., Gnesi S., Lenzini G., Petrocchi M.
Driven by and dependent on ICT, like almost everything today, railway transportation has become a critical infrastructure and, as such, is exposed to threats against communication of on-board and wayside components. The shift to cybersecurity brings up the need to comply with new security requirements, and once more security software engineers are confronted with a well-known problem: how to express informal requirements into unambiguous formal expressions that can be translated into enforceable policies or be used to verify the security of a system design. We have experience in translating natural language requirements from standards, regulations, and guidelines into Controlled Natural Language for Data Sharing Agreements (CNL4DSA), a formalism that serves the purpose of bridging natural and formal expressions. The translation of requirements is challenging, calling for a rigorous process of coding agreement between researchers. Following the trend of the time, in this paper, we question whether AI and, in particular, the novel Generative Language Models, can help us with this translation exercise. Previous work shows that AI can help in writing security code, although not always producing secure code; less studied is the quality of generative AI’s working with controlled natural languages in writing requirements for security compliance. Can AI be a valuable tool or companion in this endeavour too? To answer this question, we engage ChatGPT and Microsoft 365 Copilot with the same challenges that we faced when translating cybersecurity requirements for railway systems into CNL4DSA. Comparing our results from some time ago with those of the machine, we found surprising insights, showing the high potentiality of using AI in requirements engineering.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15219, pp. 186-203. Crete, Greece, 27-31/10/2024
DOI: 10.1007/978-3-031-73709-1_12
Metrics:
See at:
IRIS Cnr | IRIS Cnr | IRIS Cnr | doi.org | CNR IRIS | CNR IRIS
2024
Contribution to book
Open Access
Formal methods for industrial critical systems: 30 years of railway applications
Ter Beek M. H., Fantechi A., Gnesi S.
This paper, written in honour of Tiziana Margaria, aims to provide a comprehensive presentation of where mainstream formal methods are currently used for modelling and analysis of railway applications.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15240, pp. 327-344
DOI: 10.1007/978-3-031-73887-6_21
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Ter Beek M. H., Fantechi A., Gnesi S.
This paper, written in honour of Tiziana Margaria, aims to provide a comprehensive presentation of where mainstream formal methods are currently used for modelling and analysis of railway applications.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15240, pp. 327-344
DOI: 10.1007/978-3-031-73887-6_21
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
IRIS Cnr | IRIS Cnr | IRIS Cnr | doi.org | CNR IRIS | CNR IRIS
2024
Journal article
Open Access
Coherent modal transition systems refinement
Basile Davide, Ter Beek Maurice H., Fantechi Alessandro, Gnesi Stefania
Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Coherent MTS (CMTS) have been introduced to model Software Product Lines (SPL) based on a correspondence between the necessary and permitted modalities of MTS transitions and their associated actions, and the core and optional features of SPL. In this paper, we address open problems of the coherent fragment of MTS and introduce the notions of refinement and thorough refinement of CMTS. Most notably, we prove that refinement and thorough refinement coincide for CMTS, while it is known that this is not the case for MTS. We also define (thorough) equivalence and strong bisimilarity of both MTS and CMTS. We show their relations and, in particular, we prove that also strong bisimilarity and equivalence coincide for CMTS, whereas they do not for MTS. Finally, we extend our investigation to CMTS equipped with Constraints (MTSC), originally introduced to express alternative behaviour, and we prove that novel notions of refinement and strong thorough refinement coincide for MTSC, and so do their extensions to strong (thorough) equivalence and strong bisimilarity.Source: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, vol. 138
DOI: 10.1016/j.jlamp.2024.100954
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Formal Methods in Software Engineering 2.0, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Basile Davide, Ter Beek Maurice H., Fantechi Alessandro, Gnesi Stefania
Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Coherent MTS (CMTS) have been introduced to model Software Product Lines (SPL) based on a correspondence between the necessary and permitted modalities of MTS transitions and their associated actions, and the core and optional features of SPL. In this paper, we address open problems of the coherent fragment of MTS and introduce the notions of refinement and thorough refinement of CMTS. Most notably, we prove that refinement and thorough refinement coincide for CMTS, while it is known that this is not the case for MTS. We also define (thorough) equivalence and strong bisimilarity of both MTS and CMTS. We show their relations and, in particular, we prove that also strong bisimilarity and equivalence coincide for CMTS, whereas they do not for MTS. Finally, we extend our investigation to CMTS equipped with Constraints (MTSC), originally introduced to express alternative behaviour, and we prove that novel notions of refinement and strong thorough refinement coincide for MTSC, and so do their extensions to strong (thorough) equivalence and strong bisimilarity.Source: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, vol. 138
DOI: 10.1016/j.jlamp.2024.100954
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Formal Methods in Software Engineering 2.0, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
See at:
Journal of Logical and Algebraic Methods in Programming | IRIS Cnr | IRIS Cnr | CNR IRIS
2023
Conference article
Open Access
Rule-based NLP vs ChatGPT in ambiguity detection, a preliminary study
Fantechi A, Gnesi S, Semini L
With the rapid advances of AI-based tools, the question of whether to use such tools or conventional rule-based tools often arises in many application domains. In this paper, we address this question when considering the issue of ambiguity in requirements documents. For this purpose, we consider GPT-3 that is the third-generation of the Generative Pretrained Transformer language model, developed by OpenAI and we compare its ambiguity detection capability with that of a publicly available rule-based NLP tool on a few example requirements documents.Source: CEUR WORKSHOP PROCEEDINGS. Barcelona, Spain, 17-20/04/2023
Fantechi A, Gnesi S, Semini L
With the rapid advances of AI-based tools, the question of whether to use such tools or conventional rule-based tools often arises in many application domains. In this paper, we address this question when considering the issue of ambiguity in requirements documents. For this purpose, we consider GPT-3 that is the third-generation of the Generative Pretrained Transformer language model, developed by OpenAI and we compare its ambiguity detection capability with that of a publicly available rule-based NLP tool on a few example requirements documents.Source: CEUR WORKSHOP PROCEEDINGS. Barcelona, Spain, 17-20/04/2023
See at:
ceur-ws.org | CNR IRIS | ISTI Repository | CNR IRIS
2022
Journal article
Open Access
VIBE: looking for Variability In amBiguous rEquirements
Fantechi A, Gnesi S, Semini L
Variability is a characteristic of a software project and describes the fact that a system can be configured in different ways, obtaining different products (variants) from a common code base, accordingly to the software product line paradigm. This paradigm can be conveniently applied in all phases of the software process, starting from the definition and analysis of the requirements. We observe that often requirements contain ambiguities which can reveal an unintentional and implicit source of variability, that has to be detected. To this end we define VIBE, a tool supported process to identify variability aspects in requirements documents. VIBE is defined on the basis of a study of the different sources of ambiguity in natural language requirements documents that are useful to recognize potential variability, and is characterized by the use of a NLP tool customized to detect variability indicators. The tool to be used in VIBE is selected from a number of ambiguity detection tools, after a comparison of their customization features. The validation of VIBE is conducted using real-world requirements documents.Source: THE JOURNAL OF SYSTEMS AND SOFTWARE, vol. 195
DOI: 10.1016/j.jss.2022.111540
Metrics:
Fantechi A, Gnesi S, Semini L
Variability is a characteristic of a software project and describes the fact that a system can be configured in different ways, obtaining different products (variants) from a common code base, accordingly to the software product line paradigm. This paradigm can be conveniently applied in all phases of the software process, starting from the definition and analysis of the requirements. We observe that often requirements contain ambiguities which can reveal an unintentional and implicit source of variability, that has to be detected. To this end we define VIBE, a tool supported process to identify variability aspects in requirements documents. VIBE is defined on the basis of a study of the different sources of ambiguity in natural language requirements documents that are useful to recognize potential variability, and is characterized by the use of a NLP tool customized to detect variability indicators. The tool to be used in VIBE is selected from a number of ambiguity detection tools, after a comparison of their customization features. The validation of VIBE is conducted using real-world requirements documents.Source: THE JOURNAL OF SYSTEMS AND SOFTWARE, vol. 195
DOI: 10.1016/j.jss.2022.111540
Metrics:
See at:
CNR IRIS | www.sciencedirect.com | Journal of Systems and Software | CNR IRIS
2022
Conference article
Restricted
Formal methods for distributed control systems of future railways
Fantechi A, Gnesi S, Haxthausen Ae
The adoption of formal methods in railway signalling has been the subject of specific tracks of past ISOLA conferences since a decade.DOI: 10.1007/978-3-031-19762-8_19
Metrics:
Fantechi A, Gnesi S, Haxthausen Ae
The adoption of formal methods in railway signalling has been the subject of specific tracks of past ISOLA conferences since a decade.DOI: 10.1007/978-3-031-19762-8_19
Metrics:
See at:
doi.org | CNR IRIS | CNR IRIS | link.springer.com
2021
Conference article
Open Access
Formal analysis of the UNISIG safety application intermediate sub-layer. Applying Formal Methods to railway standard interfaces
Basile D, Fantechi A, Rosadi I
The combined use of standard interfaces and formal methods is currently under investigation by Shift2Rail, a joint undertaking between railway stakeholders and the EU. Standard interfaces are useful to increase market competition and standardization whilst reducing long-term life cycle costs. Formal methods are needed to achieve interoperability and safety of standard interfaces and are one of the targets of the 4SECURail project funded by Shift2Rail. This paper presents the modelling and analysis of the selected case study of the 4SECURail project: the Safe Application Intermediate sub-layer of the UNISIG RBC/RBC Safe Communication Interface. The adopted formal method is Statistical Model Checking of a network of Stochastic Priced Timed Automata, as provided by the Uppaal SMC tool. The main contributions are: (i) rigorous complete and publicly available models of an official interface specification already in operation, (ii) identification of safety and interoperability issues in the original specification using Statistical Model Checking, (iii) quantification of costs for learning the adopted formal method and developing the carried out analysis.DOI: 10.1007/978-3-030-85248-1_11
Project(s): 4SECURAIL
Metrics:
Basile D, Fantechi A, Rosadi I
The combined use of standard interfaces and formal methods is currently under investigation by Shift2Rail, a joint undertaking between railway stakeholders and the EU. Standard interfaces are useful to increase market competition and standardization whilst reducing long-term life cycle costs. Formal methods are needed to achieve interoperability and safety of standard interfaces and are one of the targets of the 4SECURail project funded by Shift2Rail. This paper presents the modelling and analysis of the selected case study of the 4SECURail project: the Safe Application Intermediate sub-layer of the UNISIG RBC/RBC Safe Communication Interface. The adopted formal method is Statistical Model Checking of a network of Stochastic Priced Timed Automata, as provided by the Uppaal SMC tool. The main contributions are: (i) rigorous complete and publicly available models of an official interface specification already in operation, (ii) identification of safety and interoperability issues in the original specification using Statistical Model Checking, (iii) quantification of costs for learning the adopted formal method and developing the carried out analysis.DOI: 10.1007/978-3-030-85248-1_11
Project(s): 4SECURAIL
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS
2021
Other
Open Access
Analysing a safe communication protocol in the railway signaling domain with Timed Automata and Statistical Model Checking
Rosadi I.
This thesis focuses on the modeling and the safety requirements verification of a communication system in the railway signaling domain, where the use of standard interfaces and formal methods is increasing and is also expanding at the industrial level.Project(s): 4SECURAIL
Rosadi I.
This thesis focuses on the modeling and the safety requirements verification of a communication system in the railway signaling domain, where the use of standard interfaces and formal methods is increasing and is also expanding at the industrial level.Project(s): 4SECURAIL
See at:
ISTI Repository | sol.unifi.it | CNR ExploRA
2020
Conference article
Open Access
Comparing formal tools for system design: a judgment study
Ferrari A, Mazzanti F., 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.DOI: 10.1145/3377811.3380373
Project(s): 4SECURAIL, ASTRail
Metrics:
Ferrari A, Mazzanti F., 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.DOI: 10.1145/3377811.3380373
Project(s): 4SECURAIL
, ASTRail Metrics:
See at:
2020.icse-conferences.org | CNR IRIS | ISTI Repository | doi.org | CNR IRIS | CNR IRIS
2020
Conference article
Open Access
Designing a demonstrator of formal methods for railways infrastructure managers
Basile D, Ter Beek Mh, 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.DOI: 10.1007/978-3-030-61467-6_30
Project(s): 4SECURAIL
Metrics:
Basile D, Ter Beek Mh, 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.DOI: 10.1007/978-3-030-61467-6_30
Project(s): 4SECURAIL
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | ISTI Repository | CNR IRIS | CNR IRIS | CNR IRIS | link.springer.com
2020
Conference article
Open Access
30 years of simulation-based quantitative analysis tools: a comparison experiment between Möbius and Uppaal SMC
Basile D, Ter Beek Mh, Di Giandomenico F, Fantechi A, Gnesi S, Spagnolo Go
We provide a brief comparison of the modelling and analysis capabilities of two different formalisms and their associated simulation-based tools, acquired from experimenting with these methods and tools on one specific case study. The case study is a cyber-physical system from an industrial railway project, namely a railroad switch heater, and the quantitative properties concern energy consumption and reliability. We modelled and analysed the case study with stochastic activity networks and Möbius on the one hand and with stochastic hybrid automata and Uppaal SMC on the other hand. We give an overview of the performed experiments and highlight specific features of the two methodologies. This yields some pointers for future research and improvements.DOI: 10.1007/978-3-030-61362-4_21
Metrics:
Basile D, Ter Beek Mh, Di Giandomenico F, Fantechi A, Gnesi S, Spagnolo Go
We provide a brief comparison of the modelling and analysis capabilities of two different formalisms and their associated simulation-based tools, acquired from experimenting with these methods and tools on one specific case study. The case study is a cyber-physical system from an industrial railway project, namely a railroad switch heater, and the quantitative properties concern energy consumption and reliability. We modelled and analysed the case study with stochastic activity networks and Möbius on the one hand and with stochastic hybrid automata and Uppaal SMC on the other hand. We give an overview of the performed experiments and highlight specific features of the two methodologies. This yields some pointers for future research and improvements.DOI: 10.1007/978-3-030-61362-4_21
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | doi.org | CNR IRIS | CNR IRIS
2020
Other
Open Access
4SECURail - D.2.1: Specification of formal development demonstrator
Mazzanti F, Basile D, Fantechi A, Gnesi S, Ferrari A, Piattino A, Masullo L, Trentini D
The overall goal of the Workstream 1 "Demonstrator Development for the use of Formal Methods in Railway Environment", spreading on the activities of Tasks 2.1, 2.2, 2.3 2.4 of the 4SecuRail project is: - the definition of a "formal methods demonstrator process" (shortly Demonstrator) for the rigorous construction and analysis of system specifications (from the point of view of infrastructure managers); - the application of the Demonstrator process to a railway signalling system case study; - with the goal of performing a cost benefits analysis and the evaluation of the required learning curve for the application of this Demonstrator process This Deliverable "Specification of formal development demonstrator", describing the result of the first part of Task 2.1, presents the overall structure of the Demonstrator process and illustrates the selected choices for its architecture, both in terms of methodologies and tools. The specified formal development demonstrator will be experimented with its application to a simple initial case study in the second part of Task 2.1. The experience gained with this initial experimentation will result in the consolidation of the definition of the Demonstrator process prototype (reported in the Deliverable D2.2 of Task 2.1 "Formal development demonstrator prototype - 1st release"). The consolidated process will then be applied in Task 2.3 to the complete case study defined in Task 2.2 and that activity will provide the reference for the costs-benefits analysis of Task 2.4.Project(s): 4SECURAIL
Mazzanti F, Basile D, Fantechi A, Gnesi S, Ferrari A, Piattino A, Masullo L, Trentini D
The overall goal of the Workstream 1 "Demonstrator Development for the use of Formal Methods in Railway Environment", spreading on the activities of Tasks 2.1, 2.2, 2.3 2.4 of the 4SecuRail project is: - the definition of a "formal methods demonstrator process" (shortly Demonstrator) for the rigorous construction and analysis of system specifications (from the point of view of infrastructure managers); - the application of the Demonstrator process to a railway signalling system case study; - with the goal of performing a cost benefits analysis and the evaluation of the required learning curve for the application of this Demonstrator process This Deliverable "Specification of formal development demonstrator", describing the result of the first part of Task 2.1, presents the overall structure of the Demonstrator process and illustrates the selected choices for its architecture, both in terms of methodologies and tools. The specified formal development demonstrator will be experimented with its application to a simple initial case study in the second part of Task 2.1. The experience gained with this initial experimentation will result in the consolidation of the definition of the Demonstrator process prototype (reported in the Deliverable D2.2 of Task 2.1 "Formal development demonstrator prototype - 1st release"). The consolidated process will then be applied in Task 2.3 to the complete case study defined in Task 2.2 and that activity will provide the reference for the costs-benefits analysis of Task 2.4.Project(s): 4SECURAIL
See at:
CNR IRIS | ISTI Repository | www.4securail.eu | CNR IRIS