2022
Journal article
Embargo
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 195 (2022). doi:10.1016/j.jss.2022.111540
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 195 (2022). doi:10.1016/j.jss.2022.111540
DOI: 10.1016/j.jss.2022.111540
Metrics:
See at:
Journal of Systems and Software 
| CNR ExploRA | www.sciencedirect.com
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.Source: ISoLA 2022 - 11th International Symposium on Leveraging Applications of Formal Methods, pp. 269–285, Rhodes, Greece, 22-30/10/2022
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.Source: ISoLA 2022 - 11th International Symposium on Leveraging Applications of Formal Methods, pp. 269–285, Rhodes, Greece, 22-30/10/2022
DOI: 10.1007/978-3-031-19762-8_21
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
2022
Conference article
Restricted
Formal methods for distributed control systems of future railways
Fantechi A., Gnesi S., Haxthausen A. E.
The adoption of formal methods in railway signalling has been the subject of specific tracks of past ISOLA conferences since a decade.Source: ISoLA'22 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 243–245, Rhodes, Greece, 22-30/10/2022
DOI: 10.1007/978-3-031-19762-8_19
Metrics:
Fantechi A., Gnesi S., Haxthausen A. E.
The adoption of formal methods in railway signalling has been the subject of specific tracks of past ISOLA conferences since a decade.Source: ISoLA'22 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 243–245, Rhodes, Greece, 22-30/10/2022
DOI: 10.1007/978-3-031-19762-8_19
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
2022
Conference article
Open Access
The 4SECURail approach to formalizing standard interfaces between signalling systems components
Belli D., Fantechi A., Gnesi S., Masullo L., Mazzanti F., Pistilli G., Quadrini L., Trentini D., Vaghi C.
In the context of the Shift2Rail open call S2R-OC-IP2-01-2019, one of the two work streams of the 4SECURail project (GA 881775) pursues the objective to corroborate how a clear, rigorous standard interface specification between signalling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at consolidating the most suitable techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments. This paper discusses the main results of the project.Source: Transport Research Arena (TRA) Conference, Lisbon, Portugal, 13-14/11/2022
Project(s): 4SECURAIL
Belli D., Fantechi A., Gnesi S., Masullo L., Mazzanti F., Pistilli G., Quadrini L., Trentini D., Vaghi C.
In the context of the Shift2Rail open call S2R-OC-IP2-01-2019, one of the two work streams of the 4SECURail project (GA 881775) pursues the objective to corroborate how a clear, rigorous standard interface specification between signalling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at consolidating the most suitable techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments. This paper discusses the main results of the project.Source: Transport Research Arena (TRA) Conference, Lisbon, Portugal, 13-14/11/2022
Project(s): 4SECURAIL
See at:
ISTI Repository 
| CNR ExploRA
2021
Conference article
Open Access
Supervisory synthesis of configurable behavioural contracts with modalities
Basile D., Ter Beek M. H., Degano P., Legay A., Ferrari G. L., 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.Source: FORTE 2021 - 41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, pp. 177–181, Online conference, 14-18/06/2021
DOI: 10.1007/978-3-030-78089-0_10
Metrics:
Basile D., Ter Beek M. H., Degano P., Legay A., Ferrari G. L., 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.Source: FORTE 2021 - 41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, pp. 177–181, Online conference, 14-18/06/2021
DOI: 10.1007/978-3-030-78089-0_10
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
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.Source: SPLC '21 - 25th ACM International Systems and Software Product Line Conference, pp. 32–35, Leicester, UK, 06-11/09/2021
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.Source: SPLC '21 - 25th ACM International Systems and Software Product Line Conference, pp. 32–35, Leicester, UK, 06-11/09/2021
DOI: 10.1145/3461002.3473074
Metrics:
See at:
ISTI Repository | dl.acm.org | dl.acm.org | CNR ExploRA
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: Joint 26th International Conference on Requirements Engineering: Foundation for Software Quality Workshops, Doctoral Symposium, Live Studies Track, and Poster Track, REFSQ-JP 2020, 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: Joint 26th International Conference on Requirements Engineering: Foundation for Software Quality Workshops, Doctoral Symposium, Live Studies Track, and Poster Track, REFSQ-JP 2020, Pisa, Italy, 24-27/03/2020
See at:
ceur-ws.org | ISTI Repository | CNR ExploRA
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.Source: Integrating Research and Practice in Software Engineering, edited by Jarzabek S., Poniszewska-Mara?da A., Madeyski L., pp. 125–143, 2020
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.Source: Integrating Research and Practice in Software Engineering, edited by Jarzabek S., Poniszewska-Mara?da A., Madeyski L., pp. 125–143, 2020
DOI: 10.1007/978-3-030-26574-8_10
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2020
Conference article
Open Access
Designing a demonstrator of formal methods for railways infrastructure managers
Basile D., Ter Beek M. H., Fantechi A., Ferrari A., Gnesi S., Masullo L., Mazzanti F., Piattino A., Trentini D.
The Shift2Rail Innovation Programme (IP) is focussing on innovative technologies to enhance the overall railway market segments. Formal methods and standard interfaces have been identified as two key concepts to reduce time-to-market and costs, while ensuring safety, interoperability and standardisation. However, the decision to start using formal methods is still deemed too risky. Demonstrating technical and commercial benefits of both formal methods and standard interfaces is necessary to address the obstacles of learning curve and lack of clear cost/benefit analysis that are hindering their adoption, and this is the goal of the 4SECURail project, recently funded by the Shift2Rail IP. In this paper, we provide the reasoning and the rationale for designing the formal methods demonstrator for the 4SECURail project. The design concerns two important issues that have been analysed: (i) the usefulness of formal methods from the point of view of the infrastructure managers, (ii) the adoption of a semi-formal SysML notation within our formal methods demonstrator process.Source: ISoLA'20 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Applications, pp. 467–485, Rhodes, Greece, 20-30 October, 2020
DOI: 10.1007/978-3-030-61467-6_30
Project(s): 4SECURAIL
Metrics:
Basile D., Ter Beek M. H., Fantechi A., Ferrari A., Gnesi S., Masullo L., Mazzanti F., Piattino A., Trentini D.
The Shift2Rail Innovation Programme (IP) is focussing on innovative technologies to enhance the overall railway market segments. Formal methods and standard interfaces have been identified as two key concepts to reduce time-to-market and costs, while ensuring safety, interoperability and standardisation. However, the decision to start using formal methods is still deemed too risky. Demonstrating technical and commercial benefits of both formal methods and standard interfaces is necessary to address the obstacles of learning curve and lack of clear cost/benefit analysis that are hindering their adoption, and this is the goal of the 4SECURail project, recently funded by the Shift2Rail IP. In this paper, we provide the reasoning and the rationale for designing the formal methods demonstrator for the 4SECURail project. The design concerns two important issues that have been analysed: (i) the usefulness of formal methods from the point of view of the infrastructure managers, (ii) the adoption of a semi-formal SysML notation within our formal methods demonstrator process.Source: ISoLA'20 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Applications, pp. 467–485, Rhodes, Greece, 20-30 October, 2020
DOI: 10.1007/978-3-030-61467-6_30
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository | ISTI Repository | link.springer.com | link.springer.com | CNR ExploRA
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 M. H., Di Giandomenico F., Fantechi A., Gnesi S., Spagnolo G. O.
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.Source: ISoLA 2020 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, pp. 368–384, Rhodes, Greece, 20-30/10/2020
DOI: 10.1007/978-3-030-61362-4_21
Metrics:
Basile D., Ter Beek M. H., Di Giandomenico F., Fantechi A., Gnesi S., Spagnolo G. O.
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.Source: ISoLA 2020 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, pp. 368–384, Rhodes, Greece, 20-30/10/2020
DOI: 10.1007/978-3-030-61362-4_21
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2020
Report
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.Source: Project Report, 4SECURail, D2.1, 2020
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.Source: Project Report, 4SECURail, D2.1, 2020
Project(s): 4SECURAIL
See at:
ISTI Repository | CNR ExploRA | www.4securail.eu
2020
Conference article
Open Access
Formal Methods for Distributed Computing in Future Railway Systems
Fantechi A., Gnesi S., Haxthausen A. E.
The growingly wide deployment of ERTMS-ETCS systems on high speed lines as well as on freight corridors is already a witness to the possible achievement of high safety standards by means of distributed control algorithms, that span over geographical areas and are able to safely control large physical systems.Source: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, pp. 389–392, 20-30/10/2020
DOI: 10.1007/978-3-030-61467-6_24
Metrics:
Fantechi A., Gnesi S., Haxthausen A. E.
The growingly wide deployment of ERTMS-ETCS systems on high speed lines as well as on freight corridors is already a witness to the possible achievement of high safety standards by means of distributed control algorithms, that span over geographical areas and are able to safely control large physical systems.Source: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, pp. 389–392, 20-30/10/2020
DOI: 10.1007/978-3-030-61467-6_24
Metrics:
See at:
backend.orbit.dtu.dk | ISTI Repository | Online Research Database In Technology | link.springer.com | link.springer.com | CNR ExploRA
2020
Conference article
Open Access
Message from the chairs formaliSE 2020
Gnesi S., Plat N., Bae K., Bianculli D., Krstic S.
Welcome to FormaliSE 2020, the 8th International Conference on Formal Methods in Software Engineering. FormaliSE is a yearly conference on Formal Methods in Software Engineering. (https://www.formalise.org/). It is organized by FME (Formal Methods Europe). FormaliSE is co-located with ICSE (International Conference on Software Engineering) 2020 (https://conf.researchr.org/home/icse-2020).Source: FormaliSE '20: 8th International Conference on Formal Methods in Software Engineering, pp. vii–viii, Seoul, October 2020
Gnesi S., Plat N., Bae K., Bianculli D., Krstic S.
Welcome to FormaliSE 2020, the 8th International Conference on Formal Methods in Software Engineering. FormaliSE is a yearly conference on Formal Methods in Software Engineering. (https://www.formalise.org/). It is organized by FME (Formal Methods Europe). FormaliSE is co-located with ICSE (International Conference on Software Engineering) 2020 (https://conf.researchr.org/home/icse-2020).Source: FormaliSE '20: 8th International Conference on Formal Methods in Software Engineering, pp. vii–viii, Seoul, October 2020
See at:
dl.acm.org | ISTI Repository | CNR ExploRA
2020
Conference article
Open Access
An experience with the application of three nlp tools for the analysis of natural language requirements
Arrabito M., Fantechi A., Gnesi S., Semini L.
We report on the experience made with three Natural Language Processing analysis tools, aimed to compare their performance in detecting ambiguity and under-specification in requirements documents, and to compare them with respect to other qualities like learnability, usability, and efficiency. Two industrial tools, Requirements Scout and QVscribe, and an academic one, QuARS, are compared.Source: Quality of Information and Communications Technology 13th International Conference, QUATIC 2020, pp. 488–498, Faro, Portugal, 9-11/09/2020
DOI: 10.1007/978-3-030-58793-2_39
Metrics:
Arrabito M., Fantechi A., Gnesi S., Semini L.
We report on the experience made with three Natural Language Processing analysis tools, aimed to compare their performance in detecting ambiguity and under-specification in requirements documents, and to compare them with respect to other qualities like learnability, usability, and efficiency. Two industrial tools, Requirements Scout and QVscribe, and an academic one, QuARS, are compared.Source: Quality of Information and Communications Technology 13th International Conference, QUATIC 2020, pp. 488–498, Faro, Portugal, 9-11/09/2020
DOI: 10.1007/978-3-030-58793-2_39
Metrics:
See at:
link.springer.com | ISTI Repository | CNR ExploRA | doi.org
2019
Journal article
Open Access
On the expressiveness of modal transition systems with variability constraints
Ter Beek M., Damiani F., Gnesi S., Mazzanti F., Paolini L.
We demonstrate that modal transition systems with variability constraints are equally expressive as featured transition systems, by defining a transformation of the latter into the former, a transformation of the former into the latter, and proving the soundness and completeness of both transformations. Modal transition systems and featured transition systems are widely recognised as fundamental behavioural models for software product lines and our results thus contribute to the expressiveness hierarchy of such basic models studied in other papers published in this journal.Source: Science of computer programming (Print) 169 (2019): 1–17. doi:10.1016/j.scico.2018.09.006
DOI: 10.1016/j.scico.2018.09.006
Metrics:
Ter Beek M., Damiani F., Gnesi S., Mazzanti F., Paolini L.
We demonstrate that modal transition systems with variability constraints are equally expressive as featured transition systems, by defining a transformation of the latter into the former, a transformation of the former into the latter, and proving the soundness and completeness of both transformations. Modal transition systems and featured transition systems are widely recognised as fundamental behavioural models for software product lines and our results thus contribute to the expressiveness hierarchy of such basic models studied in other papers published in this journal.Source: Science of computer programming (Print) 169 (2019): 1–17. doi:10.1016/j.scico.2018.09.006
DOI: 10.1016/j.scico.2018.09.006
Metrics:
See at:
Archivio Istituzionale | ISTI Repository | Science of Computer Programming | CNR ExploRA | www.sciencedirect.com
2019
Conference article
Open Access
Survey on formal methods and tools in railways: the ASTRail approach
Ferrari A., Ter Beek M. H., Mazzanti F., Basile D., Fantechi A., Gnesi S., Piattino A., Trentini D.
Formal methods and tools have been widely applied to the development of railway systems during the last decades. However, no universally accepted formal framework has emerged, and railway companies wishing to introduce formal methods have little guidance for the selection of the most appropriate methods and tools to adopt. A work package (WP) of the European project ASTRail, funded under the Shift2Rail initiative, addresses this problem, by performing a survey that considers scientific literature, international projects, and practitioners' perspectives to identify a collection of formal methods and tools to be applied in railways. This paper summarises the current results of this WP. We surveyed 114 scientific publications, 44 practitioners, and 8 projects to come to a shortlist of 14 methods considered suitable for system modelling and verification in railways. The methods and tools were reviewed according to a set of functional, language-related, and quality features. The current paper extends the body of knowledge with a set of publicly available documents that can be leveraged by companies for guidance on formal methods selection in railway system development.Source: RSSRail'19 - Third International Conference on Reliability, Safety, and Security of Railway Systems, pp. 226–241, Lille, France, 04-06 June 2019
DOI: 10.1007/978-3-030-18744-6_15
Project(s): ASTRail
Metrics:
Ferrari A., Ter Beek M. H., Mazzanti F., Basile D., Fantechi A., Gnesi S., Piattino A., Trentini D.
Formal methods and tools have been widely applied to the development of railway systems during the last decades. However, no universally accepted formal framework has emerged, and railway companies wishing to introduce formal methods have little guidance for the selection of the most appropriate methods and tools to adopt. A work package (WP) of the European project ASTRail, funded under the Shift2Rail initiative, addresses this problem, by performing a survey that considers scientific literature, international projects, and practitioners' perspectives to identify a collection of formal methods and tools to be applied in railways. This paper summarises the current results of this WP. We surveyed 114 scientific publications, 44 practitioners, and 8 projects to come to a shortlist of 14 methods considered suitable for system modelling and verification in railways. The methods and tools were reviewed according to a set of functional, language-related, and quality features. The current paper extends the body of knowledge with a set of publicly available documents that can be leveraged by companies for guidance on formal methods selection in railway system development.Source: RSSRail'19 - Third International Conference on Reliability, Safety, and Security of Railway Systems, pp. 226–241, Lille, France, 04-06 June 2019
DOI: 10.1007/978-3-030-18744-6_15
Project(s): ASTRail
Metrics:
See at:
ISTI Repository | Lecture Notes in Computer Science | link.springer.com | CNR ExploRA
2019
Contribution to book
Open Access
States and Events in KandISTI: A Retrospective
Ter Beek M. H., Fantechi A., Gnesi S., Mazzanti F.
Early work on automated formal verification produced pioneering model-checking algorithms, in which system computations were modelled either as sequences of distinguished states in which the system evolves or as sequences of events or actions occurring during the system's state transitions. In both cases, automata-like structures generally known as transition systems were exploited to capture all possible computations, but still either state-based or event-based. Many years later, both views were combined in descriptions of computations as the evolution between distinguished states by means of transitions characterised by the occurrence of events, and verification tools were adapted to this more general setting. Meanwhile, the most important drive in improving verification tools concerned the complexity of models, which was attacked by algorithms capable of minimising the information needed for deciding the verification questions. One of the outcomes of this quest was local, on-the-fly model checking. Both of these lines of research, pioneered by Bernhard Steffen, are discussed in this paper in a general retrospective on state-based and event-based models of transition systems and temporal logics, followed by an overview of how this is exploited in the KandISTI model-checking environment.Source: Models, Mindsets, Meta: The What, the How, and the Why Not?, edited by Margaria T.; Graf S.; Larsen K.G., pp. 110–128. Berlin: Springer, 2019
DOI: 10.1007/978-3-030-22348-9_8
Metrics:
Ter Beek M. H., Fantechi A., Gnesi S., Mazzanti F.
Early work on automated formal verification produced pioneering model-checking algorithms, in which system computations were modelled either as sequences of distinguished states in which the system evolves or as sequences of events or actions occurring during the system's state transitions. In both cases, automata-like structures generally known as transition systems were exploited to capture all possible computations, but still either state-based or event-based. Many years later, both views were combined in descriptions of computations as the evolution between distinguished states by means of transitions characterised by the occurrence of events, and verification tools were adapted to this more general setting. Meanwhile, the most important drive in improving verification tools concerned the complexity of models, which was attacked by algorithms capable of minimising the information needed for deciding the verification questions. One of the outcomes of this quest was local, on-the-fly model checking. Both of these lines of research, pioneered by Bernhard Steffen, are discussed in this paper in a general retrospective on state-based and event-based models of transition systems and temporal logics, followed by an overview of how this is exploited in the KandISTI model-checking environment.Source: Models, Mindsets, Meta: The What, the How, and the Why Not?, edited by Margaria T.; Graf S.; Larsen K.G., pp. 110–128. Berlin: Springer, 2019
DOI: 10.1007/978-3-030-22348-9_8
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2019
Contribution to book
Open Access
From the Archives of the Formal Methods and Tools Lab: Axiomatising and Contextualising ACTL
Gnesi S., Ter Beek M. H.
We present a sound and complete axiomatisation of ACTL, an action-based version of the well-known branching-time temporal logic CTL, and place it into a historical context. ACTL was originally introduced by Rocco De Nicola together with Frits Vaandrager 30 years ago, and it has played a major role in shaping the activity of our Formal Methods and Tools Lab from the nineties to this very day.Source: Models, Languages, and Tools for Concurrent and Distributed Programming, edited by Boreale M.; Corradini F.; Loreti M.; Pugliese R., pp. 219–235. Berlin: Springer, 2019
DOI: 10.1007/978-3-030-21485-2_13
Metrics:
Gnesi S., Ter Beek M. H.
We present a sound and complete axiomatisation of ACTL, an action-based version of the well-known branching-time temporal logic CTL, and place it into a historical context. ACTL was originally introduced by Rocco De Nicola together with Frits Vaandrager 30 years ago, and it has played a major role in shaping the activity of our Formal Methods and Tools Lab from the nineties to this very day.Source: Models, Languages, and Tools for Concurrent and Distributed Programming, edited by Boreale M.; Corradini F.; Loreti M.; Pugliese R., pp. 219–235. Berlin: Springer, 2019
DOI: 10.1007/978-3-030-21485-2_13
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2019
Journal article
Open Access
Controller synthesis of service contracts with variability
Basile D., Ter Beek M. H., Degano P., Legay A., Ferrari G. L., Gnesi S., Di Giandomenico F.
Service contracts characterise the desired behavioural compliance of a composition of services. Compliance is typically defined by the fulfilment of all service requests through service offers, as dictated by a given Service-Level Agreement (SLA). Contract automata are a recently introduced formalism for specifying and composing 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. To model more fine-grained SLA and more adaptive service orchestrations, in this paper 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 prototypical tool supports the developed theory.Source: Science of computer programming (Print) 187 (2019). doi:10.1016/j.scico.2019.102344
DOI: 10.1016/j.scico.2019.102344
Metrics:
Basile D., Ter Beek M. H., Degano P., Legay A., Ferrari G. L., Gnesi S., Di Giandomenico F.
Service contracts characterise the desired behavioural compliance of a composition of services. Compliance is typically defined by the fulfilment of all service requests through service offers, as dictated by a given Service-Level Agreement (SLA). Contract automata are a recently introduced formalism for specifying and composing 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. To model more fine-grained SLA and more adaptive service orchestrations, in this paper 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 prototypical tool supports the developed theory.Source: Science of computer programming (Print) 187 (2019). doi:10.1016/j.scico.2019.102344
DOI: 10.1016/j.scico.2019.102344
Metrics:
See at:
Science of Computer Programming | Flore (Florence Research Repository) | ISTI Repository | ISTI Repository | CNR ExploRA | www.sciencedirect.com
2019
Conference article
Open Access
Adopting Formal Methods in an Industrial Setting: The Railways Case
Ter Beek M. H., Boraelv A., Fantechi A., Ferrari A., Gnesi S., Loefving C., Mazzanti F.
The railway sector has seen a large number of successful applications of formal methods and tools. However, up-to-date, structured information about the industrial usage and needs related to formal tools in railways is limited. Two Shift2Rail projects, X2Rail-2 and ASTRail, have addressed this issue by performing a systematic search over the state of the art of formal methods application in railways to identify the best used practices. As part of the work of these projects, questionnaires on formal methods and tools have been designed to gather input and guidance on the adoption of formal methods in the railway domain. Even though the questionnaires were developed independently and distributed to different audiences, the responses show a certain convergence in the replies to the questions common to both. In this paper, we present a detailed report on such convergence, drawing some indications about methods and tools that are considered to constitute the most fruitful approaches to industrial adoption.Source: FM 2019 - Third International Symposium on Formal Methods, pp. 762–772, Porto, Portugal, 7-11 October
DOI: 10.1007/978-3-030-30942-8_46
Project(s): ASTRail
Metrics:
Ter Beek M. H., Boraelv A., Fantechi A., Ferrari A., Gnesi S., Loefving C., Mazzanti F.
The railway sector has seen a large number of successful applications of formal methods and tools. However, up-to-date, structured information about the industrial usage and needs related to formal tools in railways is limited. Two Shift2Rail projects, X2Rail-2 and ASTRail, have addressed this issue by performing a systematic search over the state of the art of formal methods application in railways to identify the best used practices. As part of the work of these projects, questionnaires on formal methods and tools have been designed to gather input and guidance on the adoption of formal methods in the railway domain. Even though the questionnaires were developed independently and distributed to different audiences, the responses show a certain convergence in the replies to the questions common to both. In this paper, we present a detailed report on such convergence, drawing some indications about methods and tools that are considered to constitute the most fruitful approaches to industrial adoption.Source: FM 2019 - Third International Symposium on Formal Methods, pp. 762–772, Porto, Portugal, 7-11 October
DOI: 10.1007/978-3-030-30942-8_46
Project(s): ASTRail
Metrics:
See at:
ISTI Repository | Lecture Notes in Computer Science | link.springer.com | CNR ExploRA