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
Other
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