2024
Journal article
Open Access
Product lines of dataflows
Lienhardt M., Ter Beek M. H., Damiani F.
Data-centric parallel programming models such as dataflows are well established to implement complex concurrent software. However, in a context of a configurable software, the dataflow used in its computation might vary with respect to the selected options: this happens in particular in fields such as Computational Fluid Dynamics (CFD), where the shape of the domain in which the fluid flows and the equations used to simulate the flow are all options configuring the dataflow to execute. In this paper, we present an approach to implement product lines of dataflows, based on Delta-Oriented Programming (DOP) and term rewriting. This approach includes several analyses to check that all dataflows of a product line can be generated. Moreover, we discuss a prototype implementation of the approach and demonstrate its feasibility in practice.Source: The Journal of systems and software 210 (2024). doi:10.1016/j.jss.2023.111928
DOI: 10.1016/j.jss.2023.111928
Metrics:
Lienhardt M., Ter Beek M. H., Damiani F.
Data-centric parallel programming models such as dataflows are well established to implement complex concurrent software. However, in a context of a configurable software, the dataflow used in its computation might vary with respect to the selected options: this happens in particular in fields such as Computational Fluid Dynamics (CFD), where the shape of the domain in which the fluid flows and the equations used to simulate the flow are all options configuring the dataflow to execute. In this paper, we present an approach to implement product lines of dataflows, based on Delta-Oriented Programming (DOP) and term rewriting. This approach includes several analyses to check that all dataflows of a product line can be generated. Moreover, we discuss a prototype implementation of the approach and demonstrate its feasibility in practice.Source: The Journal of systems and software 210 (2024). doi:10.1016/j.jss.2023.111928
DOI: 10.1016/j.jss.2023.111928
Metrics:
See at:
ISTI Repository 
| ISTI Repository | www.sciencedirect.com | CNR ExploRA
2023
Contribution to book
Open Access
A case study in formal analysis of system requirements
Belli D., Mazzanti F.
One of the goals of the 4SECURail project has been to demonstrate the benefits, limits, and costs of introducing formal meth- ods in the system requirements definition process. This has been done, on an experimental basis, by applying a specific set of tools and method- ologies to a case study from the railway sector. The paper describes the approach adopted in the project and some considerations resulting from the experience.Source: Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops, edited by Masci P., Bernardeschi C., Graziani P., Koddenbrock M., Palmieri M., pp. 164–173, 2023
DOI: 10.1007/978-3-031-26236-4_14
Project(s): 4SECURAIL
Metrics:
Belli D., Mazzanti F.
One of the goals of the 4SECURail project has been to demonstrate the benefits, limits, and costs of introducing formal meth- ods in the system requirements definition process. This has been done, on an experimental basis, by applying a specific set of tools and method- ologies to a case study from the railway sector. The paper describes the approach adopted in the project and some considerations resulting from the experience.Source: Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops, edited by Masci P., Bernardeschi C., Graziani P., Koddenbrock M., Palmieri M., pp. 164–173, 2023
DOI: 10.1007/978-3-031-26236-4_14
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository | doi.org 
| link.springer.com | CNR ExploRA
2023
Conference article
Open Access
Strategies, benefits and challenges of app store-inspired requirements elicitation
Ferrari A., Spoletini P.
App store-inspired elicitation is the practice of exploring competitors' apps, to get inspiration for requirements. This activity is common among developers, but little insight is available on its practical use, advantages and possible issues. This paper aims to empirically analyse this technique in a realistic scenario, in which it is used to extend the requirements of a product that were initially captured by means of more traditional requirements elicitation interviews. Considering this scenario, we conduct an experimental simulation with 58 analysts and collect qualitative data. We perform thematic analysis of the data to identify strategies, benefits, and challenges of app store-inspired elicitation, as well as differences with respect to interviews in the considered elicitation setting. Our results show that: (1) specific guidelines and procedures are required to better conduct app store-inspired elicitation; (2) current search features made available by app stores are not suitable for this practice, and more tool support is required to help analysts in the retrieval and evaluation of competing products; (3) while interviews focus on the why dimension of requirements engineering (i.e., goals), app store-inspired elicitation focuses on how (i.e., solutions), offering indications for implementation and improved usability. Our study provides a framework for researchers to address existing challenges and suggests possible benefits to fostering app store-inspired elicitation among practitioners.Source: ICSE 2023 - 45th International Conference on Software Engineering, pp. 1290–1302, Melbourne, Australia, 14-20/05/2023
DOI: 10.1109/icse48619.2023.00114
Metrics:
Ferrari A., Spoletini P.
App store-inspired elicitation is the practice of exploring competitors' apps, to get inspiration for requirements. This activity is common among developers, but little insight is available on its practical use, advantages and possible issues. This paper aims to empirically analyse this technique in a realistic scenario, in which it is used to extend the requirements of a product that were initially captured by means of more traditional requirements elicitation interviews. Considering this scenario, we conduct an experimental simulation with 58 analysts and collect qualitative data. We perform thematic analysis of the data to identify strategies, benefits, and challenges of app store-inspired elicitation, as well as differences with respect to interviews in the considered elicitation setting. Our results show that: (1) specific guidelines and procedures are required to better conduct app store-inspired elicitation; (2) current search features made available by app stores are not suitable for this practice, and more tool support is required to help analysts in the retrieval and evaluation of competing products; (3) while interviews focus on the why dimension of requirements engineering (i.e., goals), app store-inspired elicitation focuses on how (i.e., solutions), offering indications for implementation and improved usability. Our study provides a framework for researchers to address existing challenges and suggests possible benefits to fostering app store-inspired elicitation among practitioners.Source: ICSE 2023 - 45th International Conference on Software Engineering, pp. 1290–1302, Melbourne, Australia, 14-20/05/2023
DOI: 10.1109/icse48619.2023.00114
Metrics:
See at:
ISTI Repository | dl.acm.org | CNR ExploRA
2023
Contribution to journal
Open Access
Systems and software product lines of the future
Ter Beek M. H., Schaefer I.
Source: The Journal of systems and software 199 (2023). doi:10.1016/j.jss.2023.111622
DOI: 10.1016/j.jss.2023.111622
Metrics:
Ter Beek M. H., Schaefer I.
Source: The Journal of systems and software 199 (2023). doi:10.1016/j.jss.2023.111622
DOI: 10.1016/j.jss.2023.111622
Metrics:
See at:
ISTI Repository | www.sciencedirect.com | CNR ExploRA
2023
Contribution to conference
Open Access
Digitalisation of agriculture: development and evaluation of a model-based requirements engineering process
Mannari C., Spagnolo G. O., Bacco M., Malizia A.
[Context and Motivation] The requirements elicitation process for socio-technical systems requires the involvement of diverse stakeholders with different backgrounds and skills. In these contexts, ef- fective communication between business analysts and stakeholders can be supported by model-based requirements engineering (MoDRE) strategies, which leverage diagrammatic notations as a means for information exchange. [Question/Problem] Several diagrams and approaches exist to facilitate MoDRE. However, empirical evidence on their applicability to real-world contexts with a relevant social com- ponent, and going through a process of digitalisation, is limited. Furthermore, existing approaches do not evaluate the impact that the deployment of a novel digital system has on the process and its actors. [Principal idea/Results] The research outlined in this paper aims to evaluate the joint usage of typical requirements engineer notations, namely i*, class diagrams, and business process models in the elicitation of requirements for socially-intensive systems that are going through a transformative digitalisation process. We apply these notations to represent the system-as-is, and the system-to-be, with the goal of also evaluating the impact of digitalisation. We focus on living labs (LL, i.e., networks of stakeholders participating in a socio-technical system) belonging to the agriculture domain, and provide a preliminary application on a farm that is introducing an AI-based irrigation system. [Contribution] The results show that effective communication with non-technical stakeholders is feasible with the envisioned approach. Although multiple iterations are required, agronomists and farmers are able to provide constructive feedback on the basis of the models. Furthermore, impacts in terms of additional/removed tasks and actors can be effectively characterised through business process models. As part of our overall project, we will refine the method, and then apply it in 20 living labs in the EU.Source: REFSQ 2023 - 29th International Working Conference on Requirement Engineering: Foundation for Software Quality: Posters and Tools, Barcelona, Spain, 17-20/04/2023
Mannari C., Spagnolo G. O., Bacco M., Malizia A.
[Context and Motivation] The requirements elicitation process for socio-technical systems requires the involvement of diverse stakeholders with different backgrounds and skills. In these contexts, ef- fective communication between business analysts and stakeholders can be supported by model-based requirements engineering (MoDRE) strategies, which leverage diagrammatic notations as a means for information exchange. [Question/Problem] Several diagrams and approaches exist to facilitate MoDRE. However, empirical evidence on their applicability to real-world contexts with a relevant social com- ponent, and going through a process of digitalisation, is limited. Furthermore, existing approaches do not evaluate the impact that the deployment of a novel digital system has on the process and its actors. [Principal idea/Results] The research outlined in this paper aims to evaluate the joint usage of typical requirements engineer notations, namely i*, class diagrams, and business process models in the elicitation of requirements for socially-intensive systems that are going through a transformative digitalisation process. We apply these notations to represent the system-as-is, and the system-to-be, with the goal of also evaluating the impact of digitalisation. We focus on living labs (LL, i.e., networks of stakeholders participating in a socio-technical system) belonging to the agriculture domain, and provide a preliminary application on a farm that is introducing an AI-based irrigation system. [Contribution] The results show that effective communication with non-technical stakeholders is feasible with the envisioned approach. Although multiple iterations are required, agronomists and farmers are able to provide constructive feedback on the basis of the models. Furthermore, impacts in terms of additional/removed tasks and actors can be effectively characterised through business process models. As part of our overall project, we will refine the method, and then apply it in 20 living labs in the EU.Source: REFSQ 2023 - 29th International Working Conference on Requirement Engineering: Foundation for Software Quality: Posters and Tools, Barcelona, Spain, 17-20/04/2023
See at:
ceur-ws.org | ISTI Repository | ISTI Repository | ISTI Repository | CNR ExploRA
2023
Conference article
Open Access
Remote sensing and machine learning for riparian vegetation detection and classification
Fiorentini N., Bacco M., Ferrari A., Rovai M., Brunori G.
Precise and reliable identification of riparian vegetation along rivers is of paramount importance for managing bodies, enabling them to accurately plan key duties, such as the design of river maintenance interventions. Nonetheless, manual mapping is significantly expensive in terms of time and human costs, especially when authorities have to manage extensive river networks. Accordingly, in the present paper, we propose a methodology for classifying and automatically mapping the riparian vegetation of urban rivers. Specifically, the calibration of an unsupervised (Isodata Clustering) and a supervised (Random Forest) machine learning algorithm (MLA) is carried out for the classification of the riparian vegetation detected in high-resolution (1m) aerial orthoimages. Riparian vegetation is classified using Normalized Difference Vegetation Index (NDVI) features. In the framework of this research, the Isodata Clustering slightly outperforms the Random Forest, achieving a higher level of predictive performance and reliability throughout all the computed performance metrics. Moreover, being unsupervised, it does not require ground truth information, which makes it particularly competitive in terms of annotation costs when compared with supervised algorithms, and definitely appropriate in case of limited resources. We encourage river authorities to use MLA-based tools, such as the ones we propose in this work, for mapping riparian vegetation, since they can bring relevant benefits, such as limited implementation costs, easy calibration, fast training, and adequate reliability.Source: MetroAgriFor 2023 - IEEE International Workshop on Metrology for Agriculture and Forestry, Pisa, Italy, 6-8/11/2023
Project(s): DESIRA
Fiorentini N., Bacco M., Ferrari A., Rovai M., Brunori G.
Precise and reliable identification of riparian vegetation along rivers is of paramount importance for managing bodies, enabling them to accurately plan key duties, such as the design of river maintenance interventions. Nonetheless, manual mapping is significantly expensive in terms of time and human costs, especially when authorities have to manage extensive river networks. Accordingly, in the present paper, we propose a methodology for classifying and automatically mapping the riparian vegetation of urban rivers. Specifically, the calibration of an unsupervised (Isodata Clustering) and a supervised (Random Forest) machine learning algorithm (MLA) is carried out for the classification of the riparian vegetation detected in high-resolution (1m) aerial orthoimages. Riparian vegetation is classified using Normalized Difference Vegetation Index (NDVI) features. In the framework of this research, the Isodata Clustering slightly outperforms the Random Forest, achieving a higher level of predictive performance and reliability throughout all the computed performance metrics. Moreover, being unsupervised, it does not require ground truth information, which makes it particularly competitive in terms of annotation costs when compared with supervised algorithms, and definitely appropriate in case of limited resources. We encourage river authorities to use MLA-based tools, such as the ones we propose in this work, for mapping riparian vegetation, since they can bring relevant benefits, such as limited implementation costs, easy calibration, fast training, and adequate reliability.Source: MetroAgriFor 2023 - IEEE International Workshop on Metrology for Agriculture and Forestry, Pisa, Italy, 6-8/11/2023
Project(s): DESIRA
See at:
ISTI Repository | CNR ExploRA
2023
Report
Open Access
On bisimilarity for polyhedral models and SLCS - Preliminary version
Ciancia V., Gabelaia D., Latella D., Massink M., De Vink E. P.
The notion of bisimilarity plays an important role in concurrency theory. It provides formal support to the idea of processes having "equivalent behaviour" and is a powerful tool for model reduction. Furthermore, bisimilarity typically coincides with logical equivalence of an appropriate modal logic enabling model checking to be applied on reduced models. Recently, notions of bisimilarity have been proposed also for models of space, including those based on polyhedra. The latter are central in many domains of application that exploit mesh processing and typically consist of millions of cells, the basic components of face-poset models, discrete representations of polyhedral models. This paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) for which the geometric spatial model checker PolyLogicA has been de- veloped, that is based on face-poset models. We propose a novel notion of spatial bisimilarity, called plus-minus-bisimilarity, for face-poset models. We show that it coincides with logical equivalence induced by SLCS on such models. The latter corresponds to logical equivalence (based on SLCS) on polyhedra which, in turn, coincides with simplicial bisimilarity, a notion of bisimilarity for continuous spaces.Source: ISTI Technical Report, ISTI-2023-TR/003, 2023
DOI: 10.32079/isti-tr-2023/003
Metrics:
Ciancia V., Gabelaia D., Latella D., Massink M., De Vink E. P.
The notion of bisimilarity plays an important role in concurrency theory. It provides formal support to the idea of processes having "equivalent behaviour" and is a powerful tool for model reduction. Furthermore, bisimilarity typically coincides with logical equivalence of an appropriate modal logic enabling model checking to be applied on reduced models. Recently, notions of bisimilarity have been proposed also for models of space, including those based on polyhedra. The latter are central in many domains of application that exploit mesh processing and typically consist of millions of cells, the basic components of face-poset models, discrete representations of polyhedral models. This paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) for which the geometric spatial model checker PolyLogicA has been de- veloped, that is based on face-poset models. We propose a novel notion of spatial bisimilarity, called plus-minus-bisimilarity, for face-poset models. We show that it coincides with logical equivalence induced by SLCS on such models. The latter corresponds to logical equivalence (based on SLCS) on polyhedra which, in turn, coincides with simplicial bisimilarity, a notion of bisimilarity for continuous spaces.Source: ISTI Technical Report, ISTI-2023-TR/003, 2023
DOI: 10.32079/isti-tr-2023/003
Metrics:
See at:
ISTI Repository | CNR ExploRA
2023
Conference article
Open Access
Minimisation of spatial models using branching bisimilarity
Ciancia V., Groote J. F., Latella D., Massink M., De Vink E. P.
Spatial logic and spatial model checking have great potential for traditional computer science domains and beyond. Reasoning about space involves two different conditional reachability modalities: a forward reachability, similar to that used in temporal logic, and a backward modality representing that a point can be reached from another point, under certain conditions. Since spatial models can be huge, suitable model minimisation techniques are crucial for efficient model checking. An effective minimisation method for the recent notion of spatial Compatible Path (CoPa)-bisimilarity is proposed, and shown to be correct. The core of our method is the encoding of Closure Models as Labelled Transition Systems, enabling minimisation algorithms for branching bisimulation to compute CoPa equivalence classes. Initial validation via benchmark examples demonstrates a promising speed-up in model checking of spatial properties for models of realistic size.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 263–281, Luebeck, Germany, 6-10/03/2023
DOI: 10.1007/978-3-031-27481-7_16
Metrics:
Ciancia V., Groote J. F., Latella D., Massink M., De Vink E. P.
Spatial logic and spatial model checking have great potential for traditional computer science domains and beyond. Reasoning about space involves two different conditional reachability modalities: a forward reachability, similar to that used in temporal logic, and a backward modality representing that a point can be reached from another point, under certain conditions. Since spatial models can be huge, suitable model minimisation techniques are crucial for efficient model checking. An effective minimisation method for the recent notion of spatial Compatible Path (CoPa)-bisimilarity is proposed, and shown to be correct. The core of our method is the encoding of Closure Models as Labelled Transition Systems, enabling minimisation algorithms for branching bisimulation to compute CoPa equivalence classes. Initial validation via benchmark examples demonstrates a promising speed-up in model checking of spatial properties for models of realistic size.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 263–281, Luebeck, Germany, 6-10/03/2023
DOI: 10.1007/978-3-031-27481-7_16
Metrics:
See at:
ISTI Repository | CNR ExploRA
2023
Conference article
Open Access
Can we communicate? Using dynamic logic to verify team automata
Ter Beek M. H., Cledou G., Hennicker R., Proença J.
Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receivesmust be satisfied). Previouswork focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 122–141, Lübeck, Germany, 6-10/3/2023
DOI: 10.1007/978-3-031-27481-7_9
Metrics:
Ter Beek M. H., Cledou G., Hennicker R., Proença J.
Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receivesmust be satisfied). Previouswork focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 122–141, Lübeck, Germany, 6-10/3/2023
DOI: 10.1007/978-3-031-27481-7_9
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Conference article
Open Access
A runtime environment for contract automata
Basile D., Ter Beek M. H.
Contract automata have been introduced for specifying applications through behavioural contracts and for synthesising their orchestrations as finite state automata. This paper addresses the realisation of applications from contract automata specifications. We present CARE, a new runtime environment to coordinate services implementing contracts that guarantees the adherence of the implementation to its contract. We discuss how CARE can be adopted to realise contract-based applications, its formal guarantees, and we identify the responsibilities of the involved business actors. Experiments show the benefits of adopting CARE with respect to manual implementations.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 550–567, Lübeck, Germany, 6-10/3/2023
DOI: 10.1007/978-3-031-27481-7_31
Metrics:
Basile D., Ter Beek M. H.
Contract automata have been introduced for specifying applications through behavioural contracts and for synthesising their orchestrations as finite state automata. This paper addresses the realisation of applications from contract automata specifications. We present CARE, a new runtime environment to coordinate services implementing contracts that guarantees the adherence of the implementation to its contract. We discuss how CARE can be adopted to realise contract-based applications, its formal guarantees, and we identify the responsibilities of the involved business actors. Experiments show the benefits of adopting CARE with respect to manual implementations.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 550–567, Lübeck, Germany, 6-10/3/2023
DOI: 10.1007/978-3-031-27481-7_31
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Contribution to book
Open Access
Caratteristiche, prospettive e problematicità dell'Intelligenza Artificiale
Latella D., Siroli G. P., Tamburrini G.
Breve introduzione ai concetti fondamentali sui quali si basa l'intelligenza artificiale e alle problematiche alle quali il suo uso, specie in contesti critici, puo' dare origine. Viene data una breve introduzione storica e di inquadramento. Si approfondiscono alcuni aspetti dell'apprendimento automatico e si discutono alcuni suoi limiti e problematicità.Source: Dai droni alle armi autonome. Lasciare l'Apocalisse alle macchine?, edited by Farruggia F., pp. 43–60. Milano: Franco Angeli, 2023
Latella D., Siroli G. P., Tamburrini G.
Breve introduzione ai concetti fondamentali sui quali si basa l'intelligenza artificiale e alle problematiche alle quali il suo uso, specie in contesti critici, puo' dare origine. Viene data una breve introduzione storica e di inquadramento. Si approfondiscono alcuni aspetti dell'apprendimento automatico e si discutono alcuni suoi limiti e problematicità.Source: Dai droni alle armi autonome. Lasciare l'Apocalisse alle macchine?, edited by Farruggia F., pp. 43–60. Milano: Franco Angeli, 2023
See at:
ISTI Repository | series.francoangeli.it | CNR ExploRA
2023
Journal article
Open Access
Zero-shot learning for requirements classification: an exploratory study
Alhoshan W., Ferrari A., Zhao L.
Context: Requirements engineering researchers have been experimenting with machine learning and deep learning approaches for a range of RE tasks, such as requirements classification, requirements tracing, ambiguity detection, and modelling. However, most of today's ML/DL approaches are based on supervised learning techniques, meaning that they need to be trained using a large amount of task-specific labelled training data. This constraint poses an enormous challenge to RE researchers, as the lack of labelled data makes it difficult for them to fully exploit the benefit of advanced ML/DL technologies. Objective: This paper addresses this problem by showing how a zero-shot learning approach can be used for requirements classification without using any labelled training data. We focus on the classification task because many RE tasks can be framed as classification problems. Method: The ZSL approach used in our study employs contextual word-embeddings and transformer-based language models. We demonstrate this approach through a series of experiments to perform three classification tasks: (1)FR/NFR: classification functional requirements vs non-functional requirements; (2)NFR: identification of NFR classes; (3)Security: classification of security vs non-security requirements. Results: The study shows that the ZSL approach achieves an F1 score of 0.66 for the FR/NFR task. For the NFR task, the approach yields F1~0.72-0.80, considering the most frequent classes. For the Security task, F1~0.66. All of the aforementioned F1 scores are achieved with zero-training efforts. Conclusion: This study demonstrates the potential of ZSL for requirements classification. An important implication is that it is possible to have very little or no training data to perform classification tasks. The proposed approach thus contributes to the solution of the long-standing problem of data shortage in RE.Source: Information and software technology 159 (2023). doi:10.1016/j.infsof.2023.107202
DOI: 10.1016/j.infsof.2023.107202
Metrics:
Alhoshan W., Ferrari A., Zhao L.
Context: Requirements engineering researchers have been experimenting with machine learning and deep learning approaches for a range of RE tasks, such as requirements classification, requirements tracing, ambiguity detection, and modelling. However, most of today's ML/DL approaches are based on supervised learning techniques, meaning that they need to be trained using a large amount of task-specific labelled training data. This constraint poses an enormous challenge to RE researchers, as the lack of labelled data makes it difficult for them to fully exploit the benefit of advanced ML/DL technologies. Objective: This paper addresses this problem by showing how a zero-shot learning approach can be used for requirements classification without using any labelled training data. We focus on the classification task because many RE tasks can be framed as classification problems. Method: The ZSL approach used in our study employs contextual word-embeddings and transformer-based language models. We demonstrate this approach through a series of experiments to perform three classification tasks: (1)FR/NFR: classification functional requirements vs non-functional requirements; (2)NFR: identification of NFR classes; (3)Security: classification of security vs non-security requirements. Results: The study shows that the ZSL approach achieves an F1 score of 0.66 for the FR/NFR task. For the NFR task, the approach yields F1~0.72-0.80, considering the most frequent classes. For the Security task, F1~0.66. All of the aforementioned F1 scores are achieved with zero-training efforts. Conclusion: This study demonstrates the potential of ZSL for requirements classification. An important implication is that it is possible to have very little or no training data to perform classification tasks. The proposed approach thus contributes to the solution of the long-standing problem of data shortage in RE.Source: Information and software technology 159 (2023). doi:10.1016/j.infsof.2023.107202
DOI: 10.1016/j.infsof.2023.107202
Metrics:
See at:
ISTI Repository | ISTI Repository | ISTI Repository | www.sciencedirect.com | CNR ExploRA
2023
Conference article
Unknown
Digitalising agriculture: design and development of a modelling web environment for end-users
Mannari C., Anichini E., Malizia A., Turchi T., Ferrari A., Bacco M.
Modern digital technologies have a promising potential in the development of sustainable agriculture. For example, cloud computers powered by 5G IoT components allow the development of sophisticated applications -- e.g., for food traceability, pest detection, automatic irrigation -- also making use of different AI-based techniques. At the same time, digitalisation in agriculture is considered a socio-technical process to be evaluated by different stakeholders through collaborative approaches. Model-based requirements engineering strategies, which leverage diagrammatic notations, can support information exchange between different domains. Based on the evaluation of different solutions, we found a lack of tools for designing and modelling systems accessible to end-users. Most professional tools are desktop applications based on complex interactions, limited user experience, or generalist web platforms needing more formal components. In our study, we developed a prototype of a web environment for modelling systems based on a visual language that can be exported into standard code. We aim to involve end-users in modelling their digital ecosystems as a preliminary task for developing further applications. The prototype was evaluated in a workshop with experts following the cognitive walkthrough methodology for usability inspection. The evaluation highlighted the UI requirements to support easy-to-understand visual elements and maximise the understanding of actions while limiting user errors.Source: VL/HCC 2023 - IEEE Symposium on Visual Languages and Human-Centric Computing, Washington, DC, USA, 2-6/10/2023
Mannari C., Anichini E., Malizia A., Turchi T., Ferrari A., Bacco M.
Modern digital technologies have a promising potential in the development of sustainable agriculture. For example, cloud computers powered by 5G IoT components allow the development of sophisticated applications -- e.g., for food traceability, pest detection, automatic irrigation -- also making use of different AI-based techniques. At the same time, digitalisation in agriculture is considered a socio-technical process to be evaluated by different stakeholders through collaborative approaches. Model-based requirements engineering strategies, which leverage diagrammatic notations, can support information exchange between different domains. Based on the evaluation of different solutions, we found a lack of tools for designing and modelling systems accessible to end-users. Most professional tools are desktop applications based on complex interactions, limited user experience, or generalist web platforms needing more formal components. In our study, we developed a prototype of a web environment for modelling systems based on a visual language that can be exported into standard code. We aim to involve end-users in modelling their digital ecosystems as a preliminary task for developing further applications. The prototype was evaluated in a workshop with experts following the cognitive walkthrough methodology for usability inspection. The evaluation highlighted the UI requirements to support easy-to-understand visual elements and maximise the understanding of actions while limiting user errors.Source: VL/HCC 2023 - IEEE Symposium on Visual Languages and Human-Centric Computing, Washington, DC, USA, 2-6/10/2023
See at: CNR ExploRA
2023
Conference article
Open Access
Mutant equivalence as monotonicity in parametric timed games
Basile D., Ter Beek M. H., Göttmann H., Lochau M.
The detection of faults in software systems can be enhanced effectively by model-based mutation testing. The efficiency of this technique is hindered when mutants are equivalent to the original system model, since this makes them useless. Recently, the application of model-based mutation testing to real-time systems modelled as timed games has been investigated, which has resulted in guidelines for statically avoiding equivalent mutants. In this paper, we recast this problem into the framework of parametric timed games. We then prove a correspondence between theoretical results for the detection of equivalent mutants in timed games and the property of monotonicity that is known to hold for a sub-class of parametric timed games called L/U parametric timed games. The presented results not only simplify the theory underlying the detection of equivalent mutants in timed games, but at the same time they improve the expressiveness of a known decidable fragment of parametric timed games for which monotonicity holds.Source: FormaliSE'23 - 11th IEEE/ACM International Conference on Formal Methods in Software Engineering, pp. 55–65, Melbourne, Australia, 14-15/05/2023
DOI: 10.1109/formalise58978.2023.00014
Metrics:
Basile D., Ter Beek M. H., Göttmann H., Lochau M.
The detection of faults in software systems can be enhanced effectively by model-based mutation testing. The efficiency of this technique is hindered when mutants are equivalent to the original system model, since this makes them useless. Recently, the application of model-based mutation testing to real-time systems modelled as timed games has been investigated, which has resulted in guidelines for statically avoiding equivalent mutants. In this paper, we recast this problem into the framework of parametric timed games. We then prove a correspondence between theoretical results for the detection of equivalent mutants in timed games and the property of monotonicity that is known to hold for a sub-class of parametric timed games called L/U parametric timed games. The presented results not only simplify the theory underlying the detection of equivalent mutants in timed games, but at the same time they improve the expressiveness of a known decidable fragment of parametric timed games for which monotonicity holds.Source: FormaliSE'23 - 11th IEEE/ACM International Conference on Formal Methods in Software Engineering, pp. 55–65, Melbourne, Australia, 14-15/05/2023
DOI: 10.1109/formalise58978.2023.00014
Metrics:
See at:
ISTI Repository | ieeexplore.ieee.org | CNR ExploRA
2023
Conference article
Open Access
Evaluating a language workbench: from working memory capacity to comprehension to acceptance
Broccia G., Ferrari A., Ter Beek M. H., Cazzola W., Favalli L., Bertolotti F.
Language workbenches are tools that enable the definition, reuse and composition of programming languages and their ecosystem. This breed of frameworks aims to make the development of new languages easier and more affordable. Consequently, the comprehensibility of the language used in a language workbench (i.e., the meta-language) should be an important aspect to consider and evaluate. To the best of our knowledge, although the quantitative aspects of language workbenches are often discussed in the literature, the evaluation of comprehensibility is typically neglected. Neverlang is a language workbench that enables the definition of languages with a modular approach. This paper presents a preliminary study that intends to assess the comprehensibility of Neverlang programs, evaluated in terms of users' effectiveness and efficiency in a code comprehension task. The study also investigates the relationship between Neverlang comprehensibility and the users' working memory capacity. Furthermore, we intend to capture the relationship between Neverlang comprehensibility and users' acceptance, in terms of perceived ease of use, perceived usefulness, and intention to use. Our preliminary results on 10 subjects suggest that the users' working memory capacity may be related to the ability to comprehend Neverlang programs. On the other hand, effectiveness and efficiency do not appear to be associated with an increase in users' acceptance variables.Source: ICPC'23 - 31st IEEE/ACM International Conference on Program Comprehension, pp. 54–58, Melbourne, Australia, 15-16/05/2023
DOI: 10.1109/icpc58990.2023.00017
Metrics:
Broccia G., Ferrari A., Ter Beek M. H., Cazzola W., Favalli L., Bertolotti F.
Language workbenches are tools that enable the definition, reuse and composition of programming languages and their ecosystem. This breed of frameworks aims to make the development of new languages easier and more affordable. Consequently, the comprehensibility of the language used in a language workbench (i.e., the meta-language) should be an important aspect to consider and evaluate. To the best of our knowledge, although the quantitative aspects of language workbenches are often discussed in the literature, the evaluation of comprehensibility is typically neglected. Neverlang is a language workbench that enables the definition of languages with a modular approach. This paper presents a preliminary study that intends to assess the comprehensibility of Neverlang programs, evaluated in terms of users' effectiveness and efficiency in a code comprehension task. The study also investigates the relationship between Neverlang comprehensibility and the users' working memory capacity. Furthermore, we intend to capture the relationship between Neverlang comprehensibility and users' acceptance, in terms of perceived ease of use, perceived usefulness, and intention to use. Our preliminary results on 10 subjects suggest that the users' working memory capacity may be related to the ability to comprehend Neverlang programs. On the other hand, effectiveness and efficiency do not appear to be associated with an increase in users' acceptance variables.Source: ICPC'23 - 31st IEEE/ACM International Conference on Program Comprehension, pp. 54–58, Melbourne, Australia, 15-16/05/2023
DOI: 10.1109/icpc58990.2023.00017
Metrics:
See at:
ISTI Repository | ieeexplore.ieee.org | CNR ExploRA
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: REFSQ 2023 - 29th International Working Conference on Requirement Engineering: Foundation for Software Quality: Posters and Tools, 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: REFSQ 2023 - 29th International Working Conference on Requirement Engineering: Foundation for Software Quality: Posters and Tools, Barcelona, Spain, 17-20/04/2023
See at:
ceur-ws.org | ISTI Repository | CNR ExploRA
2023
Contribution to journal
Open Access
Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2021)
Hojjat H., Massink M.
Source: Science of computer programming (Print) 225 (2023). doi:10.1016/j.scico.2022.102913
DOI: 10.1016/j.scico.2022.102913
Metrics:
Hojjat H., Massink M.
Source: Science of computer programming (Print) 225 (2023). doi:10.1016/j.scico.2022.102913
DOI: 10.1016/j.scico.2022.102913
Metrics:
See at:
ISTI Repository | Science of Computer Programming | CNR ExploRA
2023
Report
Open Access
DESIRA - D3.5 Third set of practice abstracts
Bacco F. M., Ferrari A., Berg M., Schroth C., Rendl C., Marinos-Kouris C., Toli E., Koltsida P., Ortolani L., Lepore F., Townsend L., Hardy C., Fiorentini N., Brunori G.
This document provides DESIRA's third set of practice abstracts (PAs) which is a compilation of seven PAs. Those PAs are based on the experiences, lessons learned, project actions and reporting of the WP3 activities that aimed at the development of scenarios and showcasing of technologies building on the concept of digital game changers. Tasks 3.5 'Use Case development' and 3.6 'Showcase Technologies', are the main contributing project tasks that provided concrete results on which these seven PAs, cited in this report, are based. The first five PAs provide a concise description of five use cases that were developed during the second period of the DESIRA project. An array of conducted activities inside the boundaries of five preselected Living Labs, and with the participation of those LL's stakeholders, were planned so that WP3 could culminate in the development of five technology adoption use cases. The last two PAs of this report, supplement the five aforementioned use case PAs by showcasing two additional promising technology solutions that have the potential to contribute to sustainable digital transition pathways, as those are defined by the DESIRA's theoretical framework and as reflected by the examined agro-rural-forestry settings of this project. For a thorough and detailed analysis of the methodology, activities, and outcomes that contributed to the production of the use cases and showcase technology reports, it is recommended the reading of deliverables D3.3 'Use Cases Report' and D3.4 'Showcase Technology Report' which are the foundation documents on which this deliverable is based on.Source: ISTI Project Report, DESIRA, D3.5, pp.1–19, 2023
Project(s): DESIRA
Bacco F. M., Ferrari A., Berg M., Schroth C., Rendl C., Marinos-Kouris C., Toli E., Koltsida P., Ortolani L., Lepore F., Townsend L., Hardy C., Fiorentini N., Brunori G.
This document provides DESIRA's third set of practice abstracts (PAs) which is a compilation of seven PAs. Those PAs are based on the experiences, lessons learned, project actions and reporting of the WP3 activities that aimed at the development of scenarios and showcasing of technologies building on the concept of digital game changers. Tasks 3.5 'Use Case development' and 3.6 'Showcase Technologies', are the main contributing project tasks that provided concrete results on which these seven PAs, cited in this report, are based. The first five PAs provide a concise description of five use cases that were developed during the second period of the DESIRA project. An array of conducted activities inside the boundaries of five preselected Living Labs, and with the participation of those LL's stakeholders, were planned so that WP3 could culminate in the development of five technology adoption use cases. The last two PAs of this report, supplement the five aforementioned use case PAs by showcasing two additional promising technology solutions that have the potential to contribute to sustainable digital transition pathways, as those are defined by the DESIRA's theoretical framework and as reflected by the examined agro-rural-forestry settings of this project. For a thorough and detailed analysis of the methodology, activities, and outcomes that contributed to the production of the use cases and showcase technology reports, it is recommended the reading of deliverables D3.3 'Use Cases Report' and D3.4 'Showcase Technology Report' which are the foundation documents on which this deliverable is based on.Source: ISTI Project Report, DESIRA, D3.5, pp.1–19, 2023
Project(s): DESIRA
See at:
ISTI Repository | CNR ExploRA
2023
Report
Unknown
THE D.3.2.1 - AA@THE User needs, technical requirements and specifications
Pratali L., Campana M. G., Delmastro F., Di Martino F., Pescosolido L., Barsocchi P., Broccia G., Ciancia V., Gennaro C., Girolami M., Lagani G., La Rosa D., Latella D., Magrini M., Manca M., Massink M., Mattioli A., Moroni D., Palumbo F., Paradisi P., Paternò F., Santoro C., Sebastiani L., Vairo C.
Deliverable D3.2.1 del progetto PNRR Ecosistemi ed innovazione - THESource: ISTI Project Report, THE, D3.2, 2023
Pratali L., Campana M. G., Delmastro F., Di Martino F., Pescosolido L., Barsocchi P., Broccia G., Ciancia V., Gennaro C., Girolami M., Lagani G., La Rosa D., Latella D., Magrini M., Manca M., Massink M., Mattioli A., Moroni D., Palumbo F., Paradisi P., Paternò F., Santoro C., Sebastiani L., Vairo C.
Deliverable D3.2.1 del progetto PNRR Ecosistemi ed innovazione - THESource: ISTI Project Report, THE, D3.2, 2023
See at: CNR ExploRA
2023
Conference article
Open Access
On bisimilarity for polyhedral models and SLCS
Ciancia V., Gabelaia D., Latella D., Massink M., De Vink E. P.
The notion of bisimilarity plays an important role in con- currency theory. It provides formal support to the idea of processes hav- ing "equivalent behaviour" and is a powerful tool for model reduction. Furthermore, bisimilarity typically coincides with logical equivalence of an appropriate modal logic enabling model checking to be applied on reduced models. Recently, notions of bisimilarity have been proposed also for models of space, including those based on polyhedra. The latter are central in many domains of application that exploit mesh processing and typically consist of millions of cells, the basic components of face- poset models, discrete representations of polyhedral models. This paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) for which the geometric spatial model checker PolyLogicA has been developed, that is based on face-poset models. We propose a novel notion of spatial bisimilarity for face-poset models, called ±-bisimilarity. We show that it coincides with logical equivalence induced by SLCS on such models. The latter corresponds to logical equivalence with respect to SLCS on polyhedra which, in turn, coincides with simplicial bisimilarity, a notion of bisimilarity for continuous spaces.Source: DisCoTec 2023 - 43rd IFIP WG 6.1 International Conference, FORTE 2023 Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, pp. 132–151, Lisbon, Portugal, 19-23/06/2023
DOI: 10.1007/978-3-031-35355-0_9
Metrics:
Ciancia V., Gabelaia D., Latella D., Massink M., De Vink E. P.
The notion of bisimilarity plays an important role in con- currency theory. It provides formal support to the idea of processes hav- ing "equivalent behaviour" and is a powerful tool for model reduction. Furthermore, bisimilarity typically coincides with logical equivalence of an appropriate modal logic enabling model checking to be applied on reduced models. Recently, notions of bisimilarity have been proposed also for models of space, including those based on polyhedra. The latter are central in many domains of application that exploit mesh processing and typically consist of millions of cells, the basic components of face- poset models, discrete representations of polyhedral models. This paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) for which the geometric spatial model checker PolyLogicA has been developed, that is based on face-poset models. We propose a novel notion of spatial bisimilarity for face-poset models, called ±-bisimilarity. We show that it coincides with logical equivalence induced by SLCS on such models. The latter corresponds to logical equivalence with respect to SLCS on polyhedra which, in turn, coincides with simplicial bisimilarity, a notion of bisimilarity for continuous spaces.Source: DisCoTec 2023 - 43rd IFIP WG 6.1 International Conference, FORTE 2023 Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, pp. 132–151, Lisbon, Portugal, 19-23/06/2023
DOI: 10.1007/978-3-031-35355-0_9
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Conference article
Open Access
ModeLLer - a prototype to support requirements elicitation in co-design environments
Mannari C., Anichini E., Bacco M., Ferrari A., Turchi T., Malizia A.
This contribution presents ModeLLer, a prototype of a web tool for system modelling based on a block-based visual editor. The aim of ModeLLer is to enable collaborative environments in requirements elicitation, allowing end-users to create UML class diagrams without any knowledge of the (semi-)formal UML notation.Source: RE 2023 - 31st IEEE International Requirements Engineering Conference, Hannover, Germany, 04-08/09/2023
Mannari C., Anichini E., Bacco M., Ferrari A., Turchi T., Malizia A.
This contribution presents ModeLLer, a prototype of a web tool for system modelling based on a block-based visual editor. The aim of ModeLLer is to enable collaborative environments in requirements elicitation, allowing end-users to create UML class diagrams without any knowledge of the (semi-)formal UML notation.Source: RE 2023 - 31st IEEE International Requirements Engineering Conference, Hannover, Germany, 04-08/09/2023
See at:
ISTI Repository | CNR ExploRA
2023
Conference article
Open Access
Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect
Basile D., Mazzanti F., Ferrari A.
The use of formal methods can reduce the time and costs associated with railway signalling systems development and maintenance, and improve correct behaviour and safety. The integration of formal methods into industrial model-based development tools has been the subject of recent research, indicating the potential transfer of academic techniques to enhance industrial tools. This paper explores the integration of an academic formal verification tool, UML Model Checker (UMC), with an industrial model-based development tool, Sparx Enterprise Architect (Sparx EA). The case study being analyzed is a railway standard interface. The paper demonstrates how formal verification techniques from academic tools can be integrated into industrial development practices using industrial tools, and how simulation in Sparx EA can be derived from traces generated by the UMC formal verification activity. From this experience, we derive a set of lessons learned and research challenges.Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 1–21, Antwerp, Belgium, 20-22/09/2023
DOI: 10.1007/978-3-031-43681-9_1
Project(s): 4SECURAIL
Metrics:
Basile D., Mazzanti F., Ferrari A.
The use of formal methods can reduce the time and costs associated with railway signalling systems development and maintenance, and improve correct behaviour and safety. The integration of formal methods into industrial model-based development tools has been the subject of recent research, indicating the potential transfer of academic techniques to enhance industrial tools. This paper explores the integration of an academic formal verification tool, UML Model Checker (UMC), with an industrial model-based development tool, Sparx Enterprise Architect (Sparx EA). The case study being analyzed is a railway standard interface. The paper demonstrates how formal verification techniques from academic tools can be integrated into industrial development practices using industrial tools, and how simulation in Sparx EA can be derived from traces generated by the UMC formal verification activity. From this experience, we derive a set of lessons learned and research challenges.Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 1–21, Antwerp, Belgium, 20-22/09/2023
DOI: 10.1007/978-3-031-43681-9_1
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Conference article
Open Access
Research challenges in orchestration synthesis
Basile D., Ter Beek M. H.
Contract automata allow to formally define the behaviour of service contracts in terms of service offers and requests, some of which are moreover optional and some of which are necessary. A composition of contracts is said to be in agreement if all service requests are matched by corresponding offers. Whenever a composition of contracts is not in agreement, it can be refined to reach an agreement using the orchestration synthesis algorithm. This algorithm is a variant of the synthesis algorithm used in supervisory control theory and it is based on the fact that optional transitions are controllable, whereas necessary transitions are at most semi-controllable and cannot always be controlled. In fact, the resulting orchestration is such that as much of the behaviour in agreement is maintained. In this paper, we discuss recent developments of the orchestration synthesis algorithm for contract automata. Notably, we present a refined notion of semi-controllability and compare it with the original notion by means of examples. We then discuss the current limits of the orchestration synthesis algorithm and identify a number of research challenges together with a research roadmap.Source: ICE 2023 - 16th Interaction and Concurrency Experience, Lisbon, Portugal, 19/6/2023
DOI: 10.4204/eptcs.383.5
Metrics:
Basile D., Ter Beek M. H.
Contract automata allow to formally define the behaviour of service contracts in terms of service offers and requests, some of which are moreover optional and some of which are necessary. A composition of contracts is said to be in agreement if all service requests are matched by corresponding offers. Whenever a composition of contracts is not in agreement, it can be refined to reach an agreement using the orchestration synthesis algorithm. This algorithm is a variant of the synthesis algorithm used in supervisory control theory and it is based on the fact that optional transitions are controllable, whereas necessary transitions are at most semi-controllable and cannot always be controlled. In fact, the resulting orchestration is such that as much of the behaviour in agreement is maintained. In this paper, we discuss recent developments of the orchestration synthesis algorithm for contract automata. Notably, we present a refined notion of semi-controllability and compare it with the original notion by means of examples. We then discuss the current limits of the orchestration synthesis algorithm and identify a number of research challenges together with a research roadmap.Source: ICE 2023 - 16th Interaction and Concurrency Experience, Lisbon, Portugal, 19/6/2023
DOI: 10.4204/eptcs.383.5
Metrics:
See at:
cgi.cse.unsw.edu.au | ISTI Repository | CNR ExploRA
2023
Software
Unknown
Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect - Complementary data
Basile D., Mazzanti F., Ferrari A.
This repository contains the UMC and SPARX EA data used in the paper: Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect by Davide Basile, Franco Mazzanti and Alessio Ferrari.DOI: 10.5281/zenodo.7920448
Project(s): 4SECURAIL
Metrics:
Basile D., Mazzanti F., Ferrari A.
This repository contains the UMC and SPARX EA data used in the paper: Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect by Davide Basile, Franco Mazzanti and Alessio Ferrari.DOI: 10.5281/zenodo.7920448
Project(s): 4SECURAIL
Metrics:
See at: CNR ExploRA
2023
Software
Unknown
A toolchain for strategy synthesis with spatial properties - Complementary material
Basile D., Ter Beek M. H., Bussi L., Ciancia V.
This is the complementary material for our paper ``A Toolchain for Strategy Synthesis with Spatial Properties'' accepted for publication at the Journal of Software Tools and Technology Transfer. This repository contains a permanent snapshot of https://github.com/contractautomataproject/CATLib_PngConverter/tree/ec0938043146b008bbbcb4ed3ec79c06dd2e47d6DOI: 10.5281/zenodo.8220527
Metrics:
Basile D., Ter Beek M. H., Bussi L., Ciancia V.
This is the complementary material for our paper ``A Toolchain for Strategy Synthesis with Spatial Properties'' accepted for publication at the Journal of Software Tools and Technology Transfer. This repository contains a permanent snapshot of https://github.com/contractautomataproject/CATLib_PngConverter/tree/ec0938043146b008bbbcb4ed3ec79c06dd2e47d6DOI: 10.5281/zenodo.8220527
Metrics:
See at: CNR ExploRA
2023
Contribution to conference
Open Access
27th ACM International Systems and Software Product Line Conference (SPLC 2023). Proceedings - Volume A
Arcaini P., Ter Beek M. H., Perrouin G., Reinhartz-Berger I., Luaces M. R., 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.Source: New York: ACM Press, 2023
DOI: 10.1145/3579027
Metrics:
Arcaini P., Ter Beek M. H., Perrouin G., Reinhartz-Berger I., Luaces M. R., 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.Source: New York: ACM Press, 2023
DOI: 10.1145/3579027
Metrics:
See at:
dl.acm.org | ISTI Repository | CNR ExploRA
2023
Contribution to conference
Open Access
27th ACM International Systems and Software Product Line Conference (SPLC 2023). Proceedings - Volume B
Arcaini P., Ter Beek M. H., Perrouin G., Reinhartz-Berger I., Machado I., Vergilio S. R., Rabiser R., Yue T., Devroey X., Pinto M., 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.Source: New York: ACM Press, 2023
DOI: 10.1145/3579028
Metrics:
Arcaini P., Ter Beek M. H., Perrouin G., Reinhartz-Berger I., Machado I., Vergilio S. R., Rabiser R., Yue T., Devroey X., Pinto M., 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.Source: New York: ACM Press, 2023
DOI: 10.1145/3579028
Metrics:
See at:
dl.acm.org | ISTI Repository | CNR ExploRA
2023
Report
Open Access
Formal modelling and analysis of a self-adaptive robotic system
Päßler J., Ter Beek M. H., Damiani F., Tapia Tarifa S. L., Johnsen E. B.
Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems are often modelled as two-layered systems with a managed subsystem handling the domain concerns and a managing subsystem implementing the adaptation logic. We consider a case study of a self-adaptive robotic system; more concretely, an autonomous underwater vehicle (AUV) used for pipeline inspection. In this paper, we model and analyse it with the feature-aware probabilistic model checker ProFeat. The functionalities of the AUV are modelled in a feature model, capturing the AUV's variability. This allows us to model the managed subsystem of the AUV as a family of systems, where each family member corresponds to a valid feature configuration of the AUV. The managing subsystem of the AUV is modelled as a control layer capable of dynamically switching between such valid feature configurations, depending both on environmental and internal conditions. We use this model to analyse probabilistic reward and safety properties for the AUV.Source: ISTI Technical Report, ISTI-2023-TR/008, pp.1–18, 2023
DOI: 10.32079/isti-tr-2023/008
Metrics:
Päßler J., Ter Beek M. H., Damiani F., Tapia Tarifa S. L., Johnsen E. B.
Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems are often modelled as two-layered systems with a managed subsystem handling the domain concerns and a managing subsystem implementing the adaptation logic. We consider a case study of a self-adaptive robotic system; more concretely, an autonomous underwater vehicle (AUV) used for pipeline inspection. In this paper, we model and analyse it with the feature-aware probabilistic model checker ProFeat. The functionalities of the AUV are modelled in a feature model, capturing the AUV's variability. This allows us to model the managed subsystem of the AUV as a family of systems, where each family member corresponds to a valid feature configuration of the AUV. The managing subsystem of the AUV is modelled as a control layer capable of dynamically switching between such valid feature configurations, depending both on environmental and internal conditions. We use this model to analyse probabilistic reward and safety properties for the AUV.Source: ISTI Technical Report, ISTI-2023-TR/008, pp.1–18, 2023
DOI: 10.32079/isti-tr-2023/008
Metrics:
See at: CNR ExploRA
2023
Contribution to book
Open Access
REFSQ 2023: joint proceedings of workshops, doctoral symposium, posters & tools track, and journal early feedback track - Preface
Spagnolo G. O., Ferrari A., Penzenstadler B.
This document is the preface of the Joint Proceedings of Workshops, Doctoral Symposium, Posters & Tools Track, and Journal Early Feedback Track of the 29th International Working Conference on Requirement Engineering: Foundation for Software Quality (REFSQ 2023), 17th--20th April 2023, held in Barcelona, Catalunya, Spain.Source: Joint Proceedings of REFSQ-2023 Workshops, Doctoral Symposium, Posters & Tools Track and Journal Early Feedback co-located with the 28th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2023), edited by Ferrari A. et al., 2023
Spagnolo G. O., Ferrari A., Penzenstadler B.
This document is the preface of the Joint Proceedings of Workshops, Doctoral Symposium, Posters & Tools Track, and Journal Early Feedback Track of the 29th International Working Conference on Requirement Engineering: Foundation for Software Quality (REFSQ 2023), 17th--20th April 2023, held in Barcelona, Catalunya, Spain.Source: Joint Proceedings of REFSQ-2023 Workshops, Doctoral Symposium, Posters & Tools Track and Journal Early Feedback co-located with the 28th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2023), edited by Ferrari A. et al., 2023
See at:
ceur-ws.org | ISTI Repository | CNR ExploRA
2023
Report
Open Access
SLCS on face-poset models and bisimilarities on quasi-discrete closure models
Ciancia V., Latella D., Massink M.
We define SLCS\eta, a weaker logic than SLCS\gamma, and we interpret it on face-poset models. We show the relationship between the equivalence induced by the two logics, namely =SLCS\gamma and =SLCS\eta and bisimilarities of finite closure models proposed in the literature.Source: 10.32079/ISTI-TR-2023/009, 2023
DOI: 10.32079/isti-tr-2023/009
Metrics:
Ciancia V., Latella D., Massink M.
We define SLCS\eta, a weaker logic than SLCS\gamma, and we interpret it on face-poset models. We show the relationship between the equivalence induced by the two logics, namely =SLCS\gamma and =SLCS\eta and bisimilarities of finite closure models proposed in the literature.Source: 10.32079/ISTI-TR-2023/009, 2023
DOI: 10.32079/isti-tr-2023/009
Metrics:
See at:
ISTI Repository | CNR ExploRA
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.Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 22–39, Antwerp, Belgium, 20-22/09/2023
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.Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 22–39, Antwerp, Belgium, 20-22/09/2023
DOI: 10.1007/978-3-031-43681-9_2
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Contribution to journal
Open Access
Introduction to the special collection from iFM 2022
Monahan R., Ter Beek M. H.
Source: Formal aspects of computing 35 (2023): 1–2. doi:10.1145/3622995
DOI: 10.1145/3622995
Metrics:
Monahan R., Ter Beek M. H.
Source: Formal aspects of computing 35 (2023): 1–2. doi:10.1145/3622995
DOI: 10.1145/3622995
Metrics:
See at:
dl.acm.org | ISTI Repository | CNR ExploRA
2023
Report
Open Access
A sound and complete refinement relation for non-reducible modal transition systems
Basile D.
Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Whenever two MTS are not in modal refinement relationship, it could still be the case that the set of implementations of one MTS is included in the set of implementations of the other. The challenge of devising an alternative notion of modal refinement that is both sound and complete with respect to the set of implementations, without disregarding valuable implementations, remains open. In this paper, we address this challenge. We introduce a subset of MTS called Non-reducible Modal Transition Systems (NMTS), together with a novel refinement relation for NMTS. We show that NMTS refinement is sound and also complete with respect to its set of implementations. We illustrate through examples how the additional constraints imposed by NMTS are necessary for achieving completeness. Furthermore, we discuss a property holding for NMTS whose implementations are non-deterministic. We show that any implementation obtained through modal refinement but disregarded by NMTS refinement is violating this property.Source: ISTI Working papers, 2023
DOI: 10.48550/arxiv.2310.08412
Metrics:
Basile D.
Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Whenever two MTS are not in modal refinement relationship, it could still be the case that the set of implementations of one MTS is included in the set of implementations of the other. The challenge of devising an alternative notion of modal refinement that is both sound and complete with respect to the set of implementations, without disregarding valuable implementations, remains open. In this paper, we address this challenge. We introduce a subset of MTS called Non-reducible Modal Transition Systems (NMTS), together with a novel refinement relation for NMTS. We show that NMTS refinement is sound and also complete with respect to its set of implementations. We illustrate through examples how the additional constraints imposed by NMTS are necessary for achieving completeness. Furthermore, we discuss a property holding for NMTS whose implementations are non-deterministic. We show that any implementation obtained through modal refinement but disregarded by NMTS refinement is violating this property.Source: ISTI Working papers, 2023
DOI: 10.48550/arxiv.2310.08412
Metrics:
See at:
ISTI Repository | CNR ExploRA
2023
Report
Open Access
Modelling, verifying and testing the contract automata runtime environment with Uppaal
Basile D.
The contract automata runtime environment CARE is a distributed middleware application recently introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling and verification of CARE. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool Uppaal, utilizing exhaustive and statistical model checking techniques. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and address the issues that have been identified and fixed.Source: ISTI Working papers, 2023
Basile D.
The contract automata runtime environment CARE is a distributed middleware application recently introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling and verification of CARE. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool Uppaal, utilizing exhaustive and statistical model checking techniques. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and address the issues that have been identified and fixed.Source: ISTI Working papers, 2023
See at:
ISTI Repository | CNR ExploRA
2023
Software
Unknown
Modelling, verifying and testing the contract automata runtime environment with Uppaal: complementary data
Basile D.
This repository contains the complementary material for the paper: "Modelling and Verifying the Contract Automata Runtime Environment", Basile D. The latest version of the included files can be accessed through the GitHub repository of the Contract Automata Runtime Environment, https://github.com/contractautomataproject/CARE/tree/master/src/spec/uppaal In addition to the other contents, this Zenodo repository contains all the logs of the experiments.
Basile D.
This repository contains the complementary material for the paper: "Modelling and Verifying the Contract Automata Runtime Environment", Basile D. The latest version of the included files can be accessed through the GitHub repository of the Contract Automata Runtime Environment, https://github.com/contractautomataproject/CARE/tree/master/src/spec/uppaal In addition to the other contents, this Zenodo repository contains all the logs of the experiments.
See at: CNR ExploRA | zenodo.org
2023
Contribution to conference
Open Access
Research challenges in orchestration synthesis
Basile D.
This is the presentation of the paper "Research Challenges in Orchestration Synthesis" by Davide Basile and Maurice H. ter Beek, presented at the 16th Interaction and Concurrency Experience satellite workshop of the 18th International Federated Conference on Distributed Computing Techniques (DisCoTec 2023).Source: DisCoTec 2023 - 43rd IFIP WG 6.1 International Conference, FORTE 2023 Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, Lisbon, Portugal, 19-23/06/2023
Basile D.
This is the presentation of the paper "Research Challenges in Orchestration Synthesis" by Davide Basile and Maurice H. ter Beek, presented at the 16th Interaction and Concurrency Experience satellite workshop of the 18th International Federated Conference on Distributed Computing Techniques (DisCoTec 2023).Source: DisCoTec 2023 - 43rd IFIP WG 6.1 International Conference, FORTE 2023 Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, Lisbon, Portugal, 19-23/06/2023
See at:
ISTI Repository | youtu.be | CNR ExploRA
2023
Contribution to conference
Open Access
Experimenting with formal verification and model-based development: the case of UMC and Sparx EA
Basile D.
This is the presentation of "Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect" by Davide Basile, Franco Mazzanti, Alessio Ferrari, Presented at the 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20-22, 2023. https://doi.org/10.1007/978-3-031-43681-9_1Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, Antwerp, Belgium, 20-22/09/2023
Basile D.
This is the presentation of "Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect" by Davide Basile, Franco Mazzanti, Alessio Ferrari, Presented at the 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20-22, 2023. https://doi.org/10.1007/978-3-031-43681-9_1Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, Antwerp, Belgium, 20-22/09/2023
See at:
ISTI Repository | www.youtube.com | CNR ExploRA
2023
Contribution to conference
Open Access
A runtime environment for contract automata
Basile D.
This is the presentation of the paper "A Runtime Environment for Contract Automata", published at the 25th International Symposium on Formal Methods. The paper is available at https://doi.org/10.1007/978-3-031-27481-7_31Source: FM 2023 - Formal Methods: 25th International Symposium, Luebeck, Germany, 6-10/03/2023
Basile D.
This is the presentation of the paper "A Runtime Environment for Contract Automata", published at the 25th International Symposium on Formal Methods. The paper is available at https://doi.org/10.1007/978-3-031-27481-7_31Source: FM 2023 - Formal Methods: 25th International Symposium, Luebeck, Germany, 6-10/03/2023
See at:
ISTI Repository | youtu.be | CNR ExploRA
2023
Journal article
Open Access
A toolchain for strategy synthesis with spatial properties
Basile D., Ter Beek M. H, Bussi L., Ciancia V.
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools \texttt{CATLib} and \texttt{VoxLogicA} to interact in a fully automated way. The Contract Automata Library (\texttt{CATLib}) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (\texttt{VoxLogicA}) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with \texttt{CAT\-Lib}, while the properties to enforce are defined by means of spatial model checking of the images with \texttt{VoxLogicA}. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain's performance also considering several recent improvements.Source: International journal on software tools for technology transfer (Print) 25 (2023): 641–658. doi:10.1007/s10009-023-00730-1
DOI: 10.1007/s10009-023-00730-1
Metrics:
Basile D., Ter Beek M. H, Bussi L., Ciancia V.
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools \texttt{CATLib} and \texttt{VoxLogicA} to interact in a fully automated way. The Contract Automata Library (\texttt{CATLib}) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (\texttt{VoxLogicA}) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with \texttt{CAT\-Lib}, while the properties to enforce are defined by means of spatial model checking of the images with \texttt{VoxLogicA}. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain's performance also considering several recent improvements.Source: International journal on software tools for technology transfer (Print) 25 (2023): 641–658. doi:10.1007/s10009-023-00730-1
DOI: 10.1007/s10009-023-00730-1
Metrics:
See at:
ISTI Repository | ISTI Repository | CNR ExploRA
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.Source: RE 2023 - 31st IEEE International Requirements Engineering Conference, Hannover, Germany, 04-08/09/2023
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.Source: RE 2023 - 31st IEEE International Requirements Engineering Conference, Hannover, Germany, 04-08/09/2023
DOI: 10.1109/re57278.2023.00045
Metrics:
See at:
ieeexplore.ieee.org | CNR ExploRA
2023
Contribution to conference
Open Access
Preface. Proceedings of the First Workshop on Trends in Configurable Systems Analysis (TiCSA'23)
Ter Beek M. H., Dubslaff C.
The analysis of configurable systems, i.e., systems those behaviors depend on parameters or support various features, is challenging due to the exponential blowup arising in the number of configuration options. This volume contains the post-proceedings of TiCSA 2023, the first workshop on Trends in Configurable Systems Analysis, where current challenges and solutions in configurable systems analysis were presented and discussed.DOI: 10.4204/eptcs.392
Metrics:
Ter Beek M. H., Dubslaff C.
The analysis of configurable systems, i.e., systems those behaviors depend on parameters or support various features, is challenging due to the exponential blowup arising in the number of configuration options. This volume contains the post-proceedings of TiCSA 2023, the first workshop on Trends in Configurable Systems Analysis, where current challenges and solutions in configurable systems analysis were presented and discussed.DOI: 10.4204/eptcs.392
Metrics:
See at:
cgi.cse.unsw.edu.au | CNR ExploRA
2023
Conference article
Open Access
Formal modelling and analysis of a self-adaptive robotic system
Päßler J., Ter Beek M. H., Damiani F., Tapia Tarifa S. L., Johnsen E. B.
Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems are often modelled as two-layered systems with a managed subsystem handling the domain concerns and a managing subsystem implementing the adaptation logic. We consider a case study of a self-adaptive robotic system; more concretely, an autonomous underwater vehicle (AUV) used for pipeline inspection. In this paper, we model and analyse it with the feature-aware probabilistic model checker ProFeat. The functionalities of the AUV are modelled in a feature model, capturing the AUV's variability. This allows us to model the managed subsystem of the AUV as a family of systems, where each family member corresponds to a valid feature configuration of the AUV. The managing subsystem of the AUV is modelled as a control layer capable of dynamically switching between such valid feature configurations, depending both on environmental and internal conditions. We use this model to analyse probabilistic reward and safety properties for the AUV.Source: iFM'23 - 18th International Conference on integrated Formal Methods, pp. 343–363, Leiden, The Netherlands, 13-15/11/2023
DOI: 10.1007/978-3-031-47705-8_18
Metrics:
Päßler J., Ter Beek M. H., Damiani F., Tapia Tarifa S. L., Johnsen E. B.
Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems are often modelled as two-layered systems with a managed subsystem handling the domain concerns and a managing subsystem implementing the adaptation logic. We consider a case study of a self-adaptive robotic system; more concretely, an autonomous underwater vehicle (AUV) used for pipeline inspection. In this paper, we model and analyse it with the feature-aware probabilistic model checker ProFeat. The functionalities of the AUV are modelled in a feature model, capturing the AUV's variability. This allows us to model the managed subsystem of the AUV as a family of systems, where each family member corresponds to a valid feature configuration of the AUV. The managing subsystem of the AUV is modelled as a control layer capable of dynamically switching between such valid feature configurations, depending both on environmental and internal conditions. We use this model to analyse probabilistic reward and safety properties for the AUV.Source: iFM'23 - 18th International Conference on integrated Formal Methods, pp. 343–363, Leiden, The Netherlands, 13-15/11/2023
DOI: 10.1007/978-3-031-47705-8_18
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Conference article
Open Access
Realisability of global models of interaction
Ter Beek M. H., Hennicker R., Proença J.
We consider global models of communicating agents specified as transition systems labelled by interactions in which multiple senders and receivers can participate. A realisation of such a model is a set of local transition systems--one per agent--which are executed concurrently using synchronous communication. Our core challenge is how to check whether a global model is realisable and, if it is, how to synthesise a realisation. We identify and compare two variants to realise global interaction models, both relying on bisimulation equivalence. Then we investigate, for both variants, realisability conditions to be checked on global models. We propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. The paper is accompanied by a tool that implements realisability checks and synthesises realisations.Source: ICTAC'23 - 20th International Colloquium on Theoretical Aspects of Computing, pp. 236–255, Lima, Perù, 4-8/12/2023
DOI: 10.1007/978-3-031-47963-2_15
Metrics:
Ter Beek M. H., Hennicker R., Proença J.
We consider global models of communicating agents specified as transition systems labelled by interactions in which multiple senders and receivers can participate. A realisation of such a model is a set of local transition systems--one per agent--which are executed concurrently using synchronous communication. Our core challenge is how to check whether a global model is realisable and, if it is, how to synthesise a realisation. We identify and compare two variants to realise global interaction models, both relying on bisimulation equivalence. Then we investigate, for both variants, realisability conditions to be checked on global models. We propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. The paper is accompanied by a tool that implements realisability checks and synthesises realisations.Source: ICTAC'23 - 20th International Colloquium on Theoretical Aspects of Computing, pp. 236–255, Lima, Perù, 4-8/12/2023
DOI: 10.1007/978-3-031-47963-2_15
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Contribution to journal
Open Access
Preface. Selected papers of the 24th international conference on coordination models and languages (COORDINATION 2022)
Ter Beek M. H., Sirjani M.
Source: Logical Methods in Computer Science 19 (2023).
Ter Beek M. H., Sirjani M.
Source: Logical Methods in Computer Science 19 (2023).
See at:
lmcs.episciences.org | ISTI Repository | CNR ExploRA
2023
Conference article
Open Access
Eliciting the double-edged impact of digitalisation: a case study in rural areas
Ferrari A., Lepore F., Ortolani L., Brunori G.
Designing systems that account for sustainability concerns demands for a better understanding of the impact that digital technology interventions can have on a certain socio-technical context. However, limited studies are available about the elicitation of impact-related information from stakeholders, and strategies are particularly needed to elicit possible longterm effects, including negative ones, that go beyond the planned system goals. This paper reports a case study about the impact of digitalisation in remote mountain areas, in the context of a system for ordinary land management and hydro-geological risk control. The elicitation process was based on interviews and workshops. In the initial phase, past and present impacts were identified. In a second phase, future impacts were forecasted through the discussion of two alternative scenarios: a dystopic, technology-intensive one, and a technology-balanced one. The approach was particularly effective in identifying negative impacts. Among them, we highlight the higher stress due to the excess of connectivity, the partial reduction of decision-making abilities, and the risk of marginalisation for certain types of stakeholders. The study posits that before the elicitation of system goals, requirements engineers need to identify the socio-economic impacts of ICT technologies included in the system, as negative effects need to be properly mitigated. Our study contributes to the literature with: a set of impacts specific to the case, which can apply to similar contexts; an effective approach for impact elicitation; and a list of lessons learned from the experience.Source: RE 2023 - 31st IEEE International Requirements Engineering Conference, pp. 157–168, Hannover, Germany, 4-8/09/2023
DOI: 10.1109/re57278.2023.00024
DOI: 10.48550/arxiv.2306.05078
Metrics:
Ferrari A., Lepore F., Ortolani L., Brunori G.
Designing systems that account for sustainability concerns demands for a better understanding of the impact that digital technology interventions can have on a certain socio-technical context. However, limited studies are available about the elicitation of impact-related information from stakeholders, and strategies are particularly needed to elicit possible longterm effects, including negative ones, that go beyond the planned system goals. This paper reports a case study about the impact of digitalisation in remote mountain areas, in the context of a system for ordinary land management and hydro-geological risk control. The elicitation process was based on interviews and workshops. In the initial phase, past and present impacts were identified. In a second phase, future impacts were forecasted through the discussion of two alternative scenarios: a dystopic, technology-intensive one, and a technology-balanced one. The approach was particularly effective in identifying negative impacts. Among them, we highlight the higher stress due to the excess of connectivity, the partial reduction of decision-making abilities, and the risk of marginalisation for certain types of stakeholders. The study posits that before the elicitation of system goals, requirements engineers need to identify the socio-economic impacts of ICT technologies included in the system, as negative effects need to be properly mitigated. Our study contributes to the literature with: a set of impacts specific to the case, which can apply to similar contexts; an effective approach for impact elicitation; and a list of lessons learned from the experience.Source: RE 2023 - 31st IEEE International Requirements Engineering Conference, pp. 157–168, Hannover, Germany, 4-8/09/2023
DOI: 10.1109/re57278.2023.00024
DOI: 10.48550/arxiv.2306.05078
Metrics:
See at:
arXiv.org e-Print Archive | ISTI Repository | doi.org | doi.org | ieeexplore.ieee.org | CNR ExploRA
2023
Conference article
Open Access
Requirements classification for smart allocation: a case study in the railway industry
Bashir S., Abbas M., Ferrari A., Saadatmand M., Lindberg P.
Allocation of requirements to different teams is a typical preliminary task in large-scale system development projects. This critical activity is often performed manually and can benefit from automated requirements classification techniques. To date, limited evidence is available about the effectiveness of existing machine learning (ML) approaches for requirements classification in industrial cases. This paper aims to fill this gap by evaluating state-of-the-art language models and ML algorithms for classification in the railway industry. Since the interpretation of the results of ML systems is particularly relevant in the studied context, we also provide an information augmentation approach to complement the output of the ML-based classification. Our results show that the BERT uncased language model with the softmax classifier can allocate the requirements to different teams with a 76% F1 score when considering requirements allocation to the most frequent teams. Information augmentation provides potentially useful indications in 76% of the cases. The results confirm that currently available techniques can be applied to real-world cases, thus enabling the first step for technology transfer of automated requirements classification. The study can be useful to practitioners operating in requirements-centered contexts such as railways, where accurate requirements classification becomes crucial for better allocation of requirements to various teams.Source: RE 2023 - 31st IEEE International Requirements Engineering Conference, pp. 201–211, Hannover, Germany, 4-8/09/2023
DOI: 10.1109/re57278.2023.00028
Metrics:
Bashir S., Abbas M., Ferrari A., Saadatmand M., Lindberg P.
Allocation of requirements to different teams is a typical preliminary task in large-scale system development projects. This critical activity is often performed manually and can benefit from automated requirements classification techniques. To date, limited evidence is available about the effectiveness of existing machine learning (ML) approaches for requirements classification in industrial cases. This paper aims to fill this gap by evaluating state-of-the-art language models and ML algorithms for classification in the railway industry. Since the interpretation of the results of ML systems is particularly relevant in the studied context, we also provide an information augmentation approach to complement the output of the ML-based classification. Our results show that the BERT uncased language model with the softmax classifier can allocate the requirements to different teams with a 76% F1 score when considering requirements allocation to the most frequent teams. Information augmentation provides potentially useful indications in 76% of the cases. The results confirm that currently available techniques can be applied to real-world cases, thus enabling the first step for technology transfer of automated requirements classification. The study can be useful to practitioners operating in requirements-centered contexts such as railways, where accurate requirements classification becomes crucial for better allocation of requirements to various teams.Source: RE 2023 - 31st IEEE International Requirements Engineering Conference, pp. 201–211, Hannover, Germany, 4-8/09/2023
DOI: 10.1109/re57278.2023.00028
Metrics:
See at:
ISTI Repository | doi.org | ieeexplore.ieee.org | CNR ExploRA
2023
Contribution to conference
Open Access
Preface to Requirements Engineering: Foundation for Software Quality 2023
Ferrari A., Penzenstadler B.
This volume contains the papers presented at REFSQ 2023, the 29th International Working Conference on Requirements Engineering: Foundation for Software Quality, held on April 17-20, 2023 in Barcelona, Spain.
Ferrari A., Penzenstadler B.
This volume contains the papers presented at REFSQ 2023, the 29th International Working Conference on Requirements Engineering: Foundation for Software Quality, held on April 17-20, 2023 in Barcelona, Spain.
See at:
link.springer.com | CNR ExploRA
2023
Contribution to conference
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:
ieeexplore.ieee.org | ISTI Repository | CNR ExploRA
2023
Contribution to conference
Open Access
Artificial Intelligence in Engineering and society: blue skies, black holes, and the job of Requirements Engineers (Keynote)
Ferrari A.
The democratization of artificial intelligence (AI) has brought substantial achievements in science, engineering disciplines, and society as a whole. New technologies based on large language models, multi-modal learning, embodied AI, and the quest for artificial general intelligence (AGI) promise to further change the world's landscape as we know it. At the same time, AI's rapid and uncontrolled evolution also poses serious risks to society, such as the concentration of power, exclusion, discrimination, and manipulation of reality. The keynote will present some experiences in AI democratization, including the us- age of explainable machine learning approaches for agronomists, NLP-based solutions for railway engineers, image processing techniques for the maintenance of riverbeds, and mobile data processing in road safety assessment. . The talk will outline the latest technological advancements in AI, e.g., in healthcare and science, and will show how large language models like ChatGPT and Bing Chat can solve long-standing requirements engineering (RE) problems. For example, requirements completeness can be easily checked and addressed with simple prompts, and model generation from requirements becomes a one-click task. The keynote will then describe the risks that current AI development poses to society. Besides the increasingly convincing deep fakes, and the widely discussed risks for privacy and reputation, we must be aware of the uncontrolled speed of AI evolution. As AI continues to advance, it will replace many jobs that require intellectual skills. This could lead to a significant number of people losing their jobs, as they may not have the necessary skills to adapt to the new labour market. People and entire countries that cannot exploit technological developments will be excluded from the game, and this will cause resentment and the possible emergence of new fundamentalism. The race for semiconductors is already creating hot spots and rifts between the superpowers.Source: 31st IEEE International Requirements Engineering Conference, RE 2023, pp. 67–67, Hannover, Germany, 4-8/09/2023
DOI: 10.1109/rew57809.2023.00018
Metrics:
Ferrari A.
The democratization of artificial intelligence (AI) has brought substantial achievements in science, engineering disciplines, and society as a whole. New technologies based on large language models, multi-modal learning, embodied AI, and the quest for artificial general intelligence (AGI) promise to further change the world's landscape as we know it. At the same time, AI's rapid and uncontrolled evolution also poses serious risks to society, such as the concentration of power, exclusion, discrimination, and manipulation of reality. The keynote will present some experiences in AI democratization, including the us- age of explainable machine learning approaches for agronomists, NLP-based solutions for railway engineers, image processing techniques for the maintenance of riverbeds, and mobile data processing in road safety assessment. . The talk will outline the latest technological advancements in AI, e.g., in healthcare and science, and will show how large language models like ChatGPT and Bing Chat can solve long-standing requirements engineering (RE) problems. For example, requirements completeness can be easily checked and addressed with simple prompts, and model generation from requirements becomes a one-click task. The keynote will then describe the risks that current AI development poses to society. Besides the increasingly convincing deep fakes, and the widely discussed risks for privacy and reputation, we must be aware of the uncontrolled speed of AI evolution. As AI continues to advance, it will replace many jobs that require intellectual skills. This could lead to a significant number of people losing their jobs, as they may not have the necessary skills to adapt to the new labour market. People and entire countries that cannot exploit technological developments will be excluded from the game, and this will cause resentment and the possible emergence of new fundamentalism. The race for semiconductors is already creating hot spots and rifts between the superpowers.Source: 31st IEEE International Requirements Engineering Conference, RE 2023, pp. 67–67, Hannover, Germany, 4-8/09/2023
DOI: 10.1109/rew57809.2023.00018
Metrics:
See at:
ISTI Repository | doi.org | CNR ExploRA
2022
Report
Open Access
Minimisation of spatial models using branching bisimilarity (extended version)
Ciancia V., Groote J. F., Latella D., Massink M., De Vink E. P.
Spatial logic and spatial model checking have great poten- tial for traditional computer science domains and beyond. Reasoning about space involves two different conditional reachability modalities: a forward reachability, similar to that used in temporal logic, and a backward modality representing that a point can be reached from an- other point, under certain conditions. Since spatial models can be huge, suitable model minimisation techniques are crucial for efficient model checking. An effective minimisation method for the recent notion of spatial Compatible Path (CoPa)-bisimilarity is proposed, and shown to be correct. The core of our method is the encoding of Closure Models as La- belled Transition Systems, enabling minimisation algorithms for branching bisimulation to compute CoPa equivalence classes. Initial validation via benchmark examples demonstrates a promising speed-up in model checking of spatial properties for models of realistic size. Detailed proofs of all results are provided.Source: ISTI Technical Report, ISTI-2022-TR/027, 2022
DOI: 10.32079/isti-tr-2022/027
Metrics:
Ciancia V., Groote J. F., Latella D., Massink M., De Vink E. P.
Spatial logic and spatial model checking have great poten- tial for traditional computer science domains and beyond. Reasoning about space involves two different conditional reachability modalities: a forward reachability, similar to that used in temporal logic, and a backward modality representing that a point can be reached from an- other point, under certain conditions. Since spatial models can be huge, suitable model minimisation techniques are crucial for efficient model checking. An effective minimisation method for the recent notion of spatial Compatible Path (CoPa)-bisimilarity is proposed, and shown to be correct. The core of our method is the encoding of Closure Models as La- belled Transition Systems, enabling minimisation algorithms for branching bisimulation to compute CoPa equivalence classes. Initial validation via benchmark examples demonstrates a promising speed-up in model checking of spatial properties for models of realistic size. Detailed proofs of all results are provided.Source: ISTI Technical Report, ISTI-2022-TR/027, 2022
DOI: 10.32079/isti-tr-2022/027
Metrics:
See at:
ISTI Repository | CNR ExploRA