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
2021
Conference article
Open Access
Supervisory synthesis of configurable behavioural contracts with modalities
Basile D, Ter Beek Mh, Degano P, Legay A, Ferrari Gl, Gnesi S, Di Giandomenico F
Service contracts characterise the desired behavioural compliance of a composition of services, typically defined by the fulfilment of all service requests through service offers. Contract automata are a formalism for specifying behavioural service contracts. Based on the notion of synthesis of the most permissive controller from Supervisory Control Theory, a safe orchestration of contract automata can be computed that refines a composition into a compliant one. This short paper summarises the contributions published in [8], where we endow contract automata with two orthogonal layers of variability: (i) at the structural level, constraints over service requests and offers define different configurations of a contract automaton, depending on which requests and offers are selected or discarded; and (ii) at the behavioural level, service requests of different levels of criticality can be declared, which induces the novel notion of semi-controllability. The synthesis of orchestrations is thus extended to respect both the structural and the behavioural variability constraints. Finally, we show how to efficiently compute the orchestration of all configurations from only a subset of these configurations. A recently redesigned and refactored tool supports the developed theory.DOI: 10.1007/978-3-030-78089-0_10
Metrics:
Basile D, Ter Beek Mh, Degano P, Legay A, Ferrari Gl, Gnesi S, Di Giandomenico F
Service contracts characterise the desired behavioural compliance of a composition of services, typically defined by the fulfilment of all service requests through service offers. Contract automata are a formalism for specifying behavioural service contracts. Based on the notion of synthesis of the most permissive controller from Supervisory Control Theory, a safe orchestration of contract automata can be computed that refines a composition into a compliant one. This short paper summarises the contributions published in [8], where we endow contract automata with two orthogonal layers of variability: (i) at the structural level, constraints over service requests and offers define different configurations of a contract automaton, depending on which requests and offers are selected or discarded; and (ii) at the behavioural level, service requests of different levels of criticality can be declared, which induces the novel notion of semi-controllability. The synthesis of orchestrations is thus extended to respect both the structural and the behavioural variability constraints. Finally, we show how to efficiently compute the orchestration of all configurations from only a subset of these configurations. A recently redesigned and refactored tool supports the developed theory.DOI: 10.1007/978-3-030-78089-0_10
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS
2021
Conference article
Open Access
A spaCy-based tool for extracting variability from NL requirements
Fantechi A, Gnesi S, Livi S, Semini L
In previous work, we have shown that ambiguity detection in requirements can also be used as a way to capture latent aspects of variability. Natural Language Processing (NLP) tools have been used for a lexical analysis aimed at ambiguity indicators detection, and we have studied the necessary adaptations to those tools for pointing at potential variability, essentially by adding specific dictionaries for variability. We have identified also some syntactic rules able to detect potential variability, such as disjunction between nouns or pairs of indicators in a subordinate proposition. This paper describes a new prototype NLP tool, based on the spaCy library, specifically designed to detect variability. The prototype is shown to preserve the same recall exhibited by previously used lexical tools, with a higher precision.DOI: 10.1145/3461002.3473074
Metrics:
Fantechi A, Gnesi S, Livi S, Semini L
In previous work, we have shown that ambiguity detection in requirements can also be used as a way to capture latent aspects of variability. Natural Language Processing (NLP) tools have been used for a lexical analysis aimed at ambiguity indicators detection, and we have studied the necessary adaptations to those tools for pointing at potential variability, essentially by adding specific dictionaries for variability. We have identified also some syntactic rules able to detect potential variability, such as disjunction between nouns or pairs of indicators in a subordinate proposition. This paper describes a new prototype NLP tool, based on the spaCy library, specifically designed to detect variability. The prototype is shown to preserve the same recall exhibited by previously used lexical tools, with a higher precision.DOI: 10.1145/3461002.3473074
Metrics:
See at:
dl.acm.org | CNR IRIS | ISTI Repository | dl.acm.org | CNR IRIS | CNR IRIS
2020
Conference article
Open Access
A comparison of NLP Tools for RE to extract Variation Points
Arrabito M, Fantechi A, Gnesi S, Semini L
In the requirement engineering of software product lines, several researches have focused on exploiting NLP techniques and tools to extract information related to features and variability from requirement documents. In a previous work we have proposed the use of the tool QuARS, a NLP Tool for Requirements Analysis, showing that some of the indicators used to detect NL ambiguity can also be exploited to detect variability. In this paper we discuss a comparison of the application at this regard of QuARS and other Requirements Analysis tools presented in the last edition of NLP4RE, in particular with respect to their ability to extract potential variation points, in search of better performances and of novel indicators.Source: CEUR WORKSHOP PROCEEDINGS. Pisa, Italy, 24-27/03/2020
Arrabito M, Fantechi A, Gnesi S, Semini L
In the requirement engineering of software product lines, several researches have focused on exploiting NLP techniques and tools to extract information related to features and variability from requirement documents. In a previous work we have proposed the use of the tool QuARS, a NLP Tool for Requirements Analysis, showing that some of the indicators used to detect NL ambiguity can also be exploited to detect variability. In this paper we discuss a comparison of the application at this regard of QuARS and other Requirements Analysis tools presented in the last edition of NLP4RE, in particular with respect to their ability to extract potential variation points, in search of better performances and of novel indicators.Source: CEUR WORKSHOP PROCEEDINGS. Pisa, Italy, 24-27/03/2020
See at:
ceur-ws.org | CNR IRIS | ISTI Repository | CNR IRIS
2020
Contribution to book
Open Access
Nuts and Bolts of Extracting Variability Models from Natural Language Requirements Documents
Arganese E, Fantechi A, Gnesi S, Semini L
Natural language (NL) requirements documents are often ambiguous, and this is considered as a source of problems in the later interpretation of requirements. Ambiguity detection tools have been developed with the objective of improving the quality of requirement documents. However, defects as vagueness, optionality, weakness and multiplicity at requirements level can in some cases give an indication of possible variability, either in design and in implementation choices or configurability decisions. Variability information is actually the seed of the software engineering development practice aiming at building families of related systems, known as software product lines. Building on the results of previous analyses conducted on large and real word requirement documents, with QuARS NL analysis tool, we provide here a classification of the forms of ambiguity that indicate variation points, and we illustrate the practical aspects of the approach by means of a simple running example. To provide a more complete description of a line of software products, it is necessary to extrapolate, in addition to variability, also the common elements. To this end we propose here to take advantage of the capabilities of the REGICE tool to extract and cluster the glossary terms from the requirement documents. In summary, we introduce the combined application of two different NL processing tools to extract features and variability and use them to model a software product line.DOI: 10.1007/978-3-030-26574-8_10
Metrics:
Arganese E, Fantechi A, Gnesi S, Semini L
Natural language (NL) requirements documents are often ambiguous, and this is considered as a source of problems in the later interpretation of requirements. Ambiguity detection tools have been developed with the objective of improving the quality of requirement documents. However, defects as vagueness, optionality, weakness and multiplicity at requirements level can in some cases give an indication of possible variability, either in design and in implementation choices or configurability decisions. Variability information is actually the seed of the software engineering development practice aiming at building families of related systems, known as software product lines. Building on the results of previous analyses conducted on large and real word requirement documents, with QuARS NL analysis tool, we provide here a classification of the forms of ambiguity that indicate variation points, and we illustrate the practical aspects of the approach by means of a simple running example. To provide a more complete description of a line of software products, it is necessary to extrapolate, in addition to variability, also the common elements. To this end we propose here to take advantage of the capabilities of the REGICE tool to extract and cluster the glossary terms from the requirement documents. In summary, we introduce the combined application of two different NL processing tools to extract features and variability and use them to model a software product line.DOI: 10.1007/978-3-030-26574-8_10
Metrics:
See at:
CNR IRIS | link.springer.com | 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