2026
Book
Open Access
Preface to Journeys between formal methods and the railway industry. Essays dedicated to Alessandro Fantechi on the occasion of his 70th birthday
Ter Beek Maurice Henri, Gnesi Stefania, Haxthausen Anne E., Semini Laura
This Festschrift contains 18 contributions by collaborators, colleagues and friends of Alessandro Fantechi to celebrate his 70th birthday.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. i-xvi
DOI: 10.1007/978-3-032-12484-5
Project(s): Sustainable Mobility National Research Center
Metrics:
Ter Beek Maurice Henri, Gnesi Stefania, Haxthausen Anne E., Semini Laura
This Festschrift contains 18 contributions by collaborators, colleagues and friends of Alessandro Fantechi to celebrate his 70th birthday.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. i-xvi
DOI: 10.1007/978-3-032-12484-5
Project(s): Sustainable Mobility National Research Center
Metrics:
See at:
CNR IRIS 
| link.springer.com | CNR IRIS 
2026
Contribution to book
Open Access
Formal methods for railway systems: a survey of research and technology transfer projects
Basile Davide, Ter Beek Maurice Henri, Broccia Giovanna, Gnesi Stefania, Mazzanti Franco, Spagnolo Giorgio Oronzo, Bacherini Stefano, Becheri Carlo, Grasso Daniele, Magnani Gianluca, Tempestini Matteo, Zingoni Niccolò, Ferrari Alessio
This paper offers a retrospective on collaborative projects that involved Alessandro Fantechi and the authors over the past two decades, from the shared perspective of the Formal Methods and Tools (FMT) lab of the Italian National Research Council (CNR) and former collaborators at General Electric (GE) Transportation and Alstom. The focus is on research and technology transfer efforts in the field of formal methods for railway systems, where Alessandro Fantechi’s contributions have been central to the development and application of formal specification, model-based verification, and tool-supported analysis. Joint work in projects such as ASTRail, 4SECURail, and TRACE-IT, as well as in industrial collaborations with Alstom and GE Transportation Systems illustrates the sustained impact of these activities on both academic research and industrial practice. This contribution reflects on the evolution of these efforts, the formal methods adopted, and the outcomes achieved in terms of methodologies, tools, and integration into safety-critical development processes. It also highlights the collaborative environment fostered across institutions and organizations, which has been instrumental in advancing the use of formal methods in the railway domain.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. 31-54
DOI: 10.1007/978-3-032-12484-5_3
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Basile Davide, Ter Beek Maurice Henri, Broccia Giovanna, Gnesi Stefania, Mazzanti Franco, Spagnolo Giorgio Oronzo, Bacherini Stefano, Becheri Carlo, Grasso Daniele, Magnani Gianluca, Tempestini Matteo, Zingoni Niccolò, Ferrari Alessio
This paper offers a retrospective on collaborative projects that involved Alessandro Fantechi and the authors over the past two decades, from the shared perspective of the Formal Methods and Tools (FMT) lab of the Italian National Research Council (CNR) and former collaborators at General Electric (GE) Transportation and Alstom. The focus is on research and technology transfer efforts in the field of formal methods for railway systems, where Alessandro Fantechi’s contributions have been central to the development and application of formal specification, model-based verification, and tool-supported analysis. Joint work in projects such as ASTRail, 4SECURail, and TRACE-IT, as well as in industrial collaborations with Alstom and GE Transportation Systems illustrates the sustained impact of these activities on both academic research and industrial practice. This contribution reflects on the evolution of these efforts, the formal methods adopted, and the outcomes achieved in terms of methodologies, tools, and integration into safety-critical development processes. It also highlights the collaborative environment fostered across institutions and organizations, which has been instrumental in advancing the use of formal methods in the railway domain.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. 31-54
DOI: 10.1007/978-3-032-12484-5_3
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
CNR IRIS | link.springer.com | CNR IRIS | CNR IRIS
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
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
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
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
Restricted
Leveraging requirements elicitation through software requirement patterns and LLMs
Franch X., Gnesi S., Paccosi F., Quer C., Semini L.
[Context and motivation] Software requirement patterns (SRPs) is one of the many techniques that contribute to requirements elicitation. At this respect, the emergence of large language models (LLMs) opens the door to cost-effective strategies to create and use SRPs. Still, the stochastic nature of LLMs threatens the inherent quality of requirements reuse and consequently, that of the elicitation process. [Question/problem] In this scientific evaluation paper, we investigate whether and how LLMs can be used in order to create an SRP catalogue and elicit requirements from it. [Principal ideas/results] SRPs can be effectively extracted by querying an LLM through appropriate prompts, but still expert assessment is key in order to deliver the best results. LLM-driven generation of questions to stakeholders for eliciting requirements from these SRPs is feasible but suffers from deficiencies such as excessive number of repetitions and out of scope requirements. [Contribution] We show that (1) LLMs can be embedded into the requirements elicitation process through a pattern instantiation-based strategy, but at the same time (2) the current state of LLM technologies requires expert assessment at a large extent.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15588, pp. 261-276. Barcelona, Spain, 7-10 April 2025
DOI: 10.1007/978-3-031-88531-0_19
Metrics:
Franch X., Gnesi S., Paccosi F., Quer C., Semini L.
[Context and motivation] Software requirement patterns (SRPs) is one of the many techniques that contribute to requirements elicitation. At this respect, the emergence of large language models (LLMs) opens the door to cost-effective strategies to create and use SRPs. Still, the stochastic nature of LLMs threatens the inherent quality of requirements reuse and consequently, that of the elicitation process. [Question/problem] In this scientific evaluation paper, we investigate whether and how LLMs can be used in order to create an SRP catalogue and elicit requirements from it. [Principal ideas/results] SRPs can be effectively extracted by querying an LLM through appropriate prompts, but still expert assessment is key in order to deliver the best results. LLM-driven generation of questions to stakeholders for eliciting requirements from these SRPs is feasible but suffers from deficiencies such as excessive number of repetitions and out of scope requirements. [Contribution] We show that (1) LLMs can be embedded into the requirements elicitation process through a pattern instantiation-based strategy, but at the same time (2) the current state of LLM technologies requires expert assessment at a large extent.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15588, pp. 261-276. Barcelona, Spain, 7-10 April 2025
DOI: 10.1007/978-3-031-88531-0_19
Metrics:
See at:
biblioproxy.cnr.it | UPCommons. Portal del coneixement obert de la UPC | CNR IRIS | Recolector de Ciencia Abierta, RECOLECTA | CNR IRIS
2025
Journal article
Open Access
Quantitative dependability evaluation of train control systems in presence of uncertainty: a systematic literature review
Carnevali L., Di Giandomenico F., Fantechi A., Gnesi S., Gori G.
Technological advances in modern Train Control Systems (TCSs) promise to improve dependability of railway transportation in terms of safety, availability, and capacity, notably by employing novel distancing policies such as Moving Block (MB) signaling and Virtual Coupling (VC), fueled by advanced train localization methods such as satellite positioning. At the same time, these technological 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. Recently, various approaches have been proposed to characterize such effects through quantitative measures, leveraging formal stochastic modeling and evaluation of the TCS behavior. In this paper, we illustrate the results of a systematic review of the literature on quantitative evaluation of dependability-related attributes of TCSs under uncertainty on vital parameters. Specifically, we have finally selected 42 relevant papers, published between 2011 and 2023, that succeed in giving, through an empirical perspective and classification, a comprehensive view of current research and practice in quantitative dependability assessment of TCSs.Source: IEEE TRANSACTIONS ON INTELLIGENT TRANSPORTATION SYSTEMS, vol. 26 (issue 4), pp. 4298-4314
DOI: 10.1109/tits.2025.3530112
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Carnevali L., Di Giandomenico F., Fantechi A., Gnesi S., Gori G.
Technological advances in modern Train Control Systems (TCSs) promise to improve dependability of railway transportation in terms of safety, availability, and capacity, notably by employing novel distancing policies such as Moving Block (MB) signaling and Virtual Coupling (VC), fueled by advanced train localization methods such as satellite positioning. At the same time, these technological 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. Recently, various approaches have been proposed to characterize such effects through quantitative measures, leveraging formal stochastic modeling and evaluation of the TCS behavior. In this paper, we illustrate the results of a systematic review of the literature on quantitative evaluation of dependability-related attributes of TCSs under uncertainty on vital parameters. Specifically, we have finally selected 42 relevant papers, published between 2011 and 2023, that succeed in giving, through an empirical perspective and classification, a comprehensive view of current research and practice in quantitative dependability assessment of TCSs.Source: IEEE TRANSACTIONS ON INTELLIGENT TRANSPORTATION SYSTEMS, vol. 26 (issue 4), pp. 4298-4314
DOI: 10.1109/tits.2025.3530112
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
CNR IRIS | ieeexplore.ieee.org | IEEE Transactions on Intelligent Transportation Systems | Flore (Florence Research Repository) | CNR IRIS | 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
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
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
2023
Book
Open Access
27th ACM International Systems and Software Product Line Conference (SPLC 2023). Proceedings - Volume A
Arcaini P, Ter Beek Mh, Perrouin G, Reinhartzberger I, Luaces Mr, Schwanninger C, Ali S, Varshosaz M, Gargantini A, Gnesi S, Lochau M, Semini L, Washizaki H
Welcome to SPLC'23, the 27th ACM International Systems and Software Product Line Conference. Looking back to the previous SPLC issues, the conference has been established as a thriving ground for practitioners, researchers, and educators working in areas related to systems and software product lines. With the increasing size and complexity of software, efficiently supporting software processes becomes an extremely important task. SPLC'23 acted as a venue fostering knowledge exchange and learning about the state of the art in software product lines aswell as newpractices, trends, innovations, insights from industrial applications, and new challenges. SPLC'23 was held at Hitotsubashi Hall in Tokyo, Japan, from August 28 to September 1, 2023.DOI: 10.1145/3579027
Metrics:
Arcaini P, Ter Beek Mh, Perrouin G, Reinhartzberger I, Luaces Mr, Schwanninger C, Ali S, Varshosaz M, Gargantini A, Gnesi S, Lochau M, Semini L, Washizaki H
Welcome to SPLC'23, the 27th ACM International Systems and Software Product Line Conference. Looking back to the previous SPLC issues, the conference has been established as a thriving ground for practitioners, researchers, and educators working in areas related to systems and software product lines. With the increasing size and complexity of software, efficiently supporting software processes becomes an extremely important task. SPLC'23 acted as a venue fostering knowledge exchange and learning about the state of the art in software product lines aswell as newpractices, trends, innovations, insights from industrial applications, and new challenges. SPLC'23 was held at Hitotsubashi Hall in Tokyo, Japan, from August 28 to September 1, 2023.DOI: 10.1145/3579027
Metrics:
See at:
dl.acm.org | CNR IRIS | ISTI Repository | CNR IRIS
2023
Conference article
Open Access
The 4SECURail case study on rigorous standard interface specifications
Belli D, Fantechi A, Gnesi S, Masullo L, Mazzanti F, Quadrini L, Trentini D, Vaghi C
In the context of the Shift2Rail open call S2R-OC-IP2-01- 2019, one of the two work streams of the 4SECURail project has pursued the objective to corroborate how a clear, rigorous standard interface specification between signaling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at illustrating some usable state-of-the-art techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments.DOI: 10.1007/978-3-031-43681-9_2
Project(s): 4SECURAIL
Metrics:
Belli D, Fantechi A, Gnesi S, Masullo L, Mazzanti F, Quadrini L, Trentini D, Vaghi C
In the context of the Shift2Rail open call S2R-OC-IP2-01- 2019, one of the two work streams of the 4SECURail project has pursued the objective to corroborate how a clear, rigorous standard interface specification between signaling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at illustrating some usable state-of-the-art techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments.DOI: 10.1007/978-3-031-43681-9_2
Project(s): 4SECURAIL
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS | CNR IRIS
2023
Conference article
Restricted
Inconsistency Detection in Natural Language Requirements using ChatGPT: a Preliminary Evaluation
Fantechi A, Gnesi S, Passaro L, Semini L
With the rapid advancement of tools based on Artificial Intelligence, it is interesting to assess their usefulness in requirements engineering. In early experiments, we have seen that ChatGPT can detect inconsistency defects in natural language (NL) requirements, that traditional NLP tools cannot identify or can identify with difficulties even after domain-focused training. This study is devoted to specifically measuring the performance of ChatGPT in finding inconsistency in requirements. Positive results in this respect could lead to the use of ChatGPT to complement existing requirements analysis tools to automatically detect this important quality criterion. For this purpose, we consider GPT-3.5, the Generative Pretrained Transformer language model developed by OpenAI. We evaluate its ability to detect inconsistency by comparing its predictions with those obtained from expert judgments by students with a proven knowledge of RE issues on a few example requirements documents.DOI: 10.1109/re57278.2023.00045
Metrics:
Fantechi A, Gnesi S, Passaro L, Semini L
With the rapid advancement of tools based on Artificial Intelligence, it is interesting to assess their usefulness in requirements engineering. In early experiments, we have seen that ChatGPT can detect inconsistency defects in natural language (NL) requirements, that traditional NLP tools cannot identify or can identify with difficulties even after domain-focused training. This study is devoted to specifically measuring the performance of ChatGPT in finding inconsistency in requirements. Positive results in this respect could lead to the use of ChatGPT to complement existing requirements analysis tools to automatically detect this important quality criterion. For this purpose, we consider GPT-3.5, the Generative Pretrained Transformer language model developed by OpenAI. We evaluate its ability to detect inconsistency by comparing its predictions with those obtained from expert judgments by students with a proven knowledge of RE issues on a few example requirements documents.DOI: 10.1109/re57278.2023.00045
Metrics:
See at:
CNR IRIS | ieeexplore.ieee.org | CNR IRIS
2023
Book
Open Access
Message from the Chairs: FormaliSE 2023
Gnesi S, Plat N, Jakobs M C, Murray T, Ferrari A, Broccia G
This volume contains the papers presented at FormaliSE 2023: the 11th International Conference on Formal Methods in Software engineering, co-located with ICSE 2023, the 45th International Conference on Software Engineering.DOI: 10.1109/formalise58978.2023.00005
Metrics:
Gnesi S, Plat N, Jakobs M C, Murray T, Ferrari A, Broccia G
This volume contains the papers presented at FormaliSE 2023: the 11th International Conference on Formal Methods in Software engineering, co-located with ICSE 2023, the 45th International Conference on Software Engineering.DOI: 10.1109/formalise58978.2023.00005
Metrics:
See at:
CNR IRIS | ieeexplore.ieee.org | 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
Future train control systems: challenges for dependability assessment
Fantechi A, Gnesi S, Gori G
The prospected advent of advanced train control systems, such as moving block and virtual coupling, raises the issue of the effects that uncertainty on critical parameters (such as position or speed) can have on dependability. Several approaches to the evaluation of such effects have been proposed, typically based on a state-based formal modelling of the system behaviour. We present a survey of such proposals.DOI: 10.1007/978-3-031-19762-8_21
Metrics:
Fantechi A, Gnesi S, Gori G
The prospected advent of advanced train control systems, such as moving block and virtual coupling, raises the issue of the effects that uncertainty on critical parameters (such as position or speed) can have on dependability. Several approaches to the evaluation of such effects have been proposed, typically based on a state-based formal modelling of the system behaviour. We present a survey of such proposals.DOI: 10.1007/978-3-031-19762-8_21
Metrics:
See at:
doi.org | CNR IRIS | CNR IRIS | link.springer.com
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
2022
Conference article
Open Access
The 4SECURail approach to formalizing standard interfaces between signalling systems components
Belli D, Fantechi A, Gnesi S, Masullo L, Mazzanti F, Pistilli G, Quadrini L, Trentini D, Vaghi C
In the context of the Shift2Rail open call S2R-OC-IP2-01-2019, one of the two work streams of the 4SECURail project (GA 881775) pursues the objective to corroborate how a clear, rigorous standard interface specification between signalling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at consolidating the most suitable techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments. This paper discusses the main results of the project.Source: TRANSPORTATION RESEARCH PROCEDIA. Lisbon, Portugal, 13-14/11/2022
Project(s): 4SECURAIL
Belli D, Fantechi A, Gnesi S, Masullo L, Mazzanti F, Pistilli G, Quadrini L, Trentini D, Vaghi C
In the context of the Shift2Rail open call S2R-OC-IP2-01-2019, one of the two work streams of the 4SECURail project (GA 881775) pursues the objective to corroborate how a clear, rigorous standard interface specification between signalling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at consolidating the most suitable techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments. This paper discusses the main results of the project.Source: TRANSPORTATION RESEARCH PROCEDIA. Lisbon, Portugal, 13-14/11/2022
Project(s): 4SECURAIL
See at:
CNR IRIS | ISTI Repository | CNR IRIS