Typology
operator:
and / or
Language
operator:
and / or
Date
operator:
and / or
Rights
operator:
and / or
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
2019
Software
Unknown
MAUVE++
Manca M., Paternò F., Santoro C., Iannuzzi N., Broccia G., Pulina F.
MAUVE++(Multiguideline Accessibility and Usability Validation Environment) is a system to evaluate accessibility of websites by checking their HTML and CSS code through guidelines, it provides validation results for different types of stakeholders, and supports validation of W3C WCAG 2.1 guidelines.
Manca M., Paternò F., Santoro C., Iannuzzi N., Broccia G., Pulina F.
MAUVE++(Multiguideline Accessibility and Usability Validation Environment) is a system to evaluate accessibility of websites by checking their HTML and CSS code through guidelines, it provides validation results for different types of stakeholders, and supports validation of W3C WCAG 2.1 guidelines.
See at: mauve.isti.cnr.it | CNR ExploRA
2020
Journal article
Open Access
Flexible automatic support for web accessibility validation
Broccia G., Manca M., Paternò F., Pulina F.
Automatic support for web accessibility validation needs to evolve for several reasons The increasingly recognised importance of accessibility implies that various stakeholders, with different expertise, look at it from different viewpoints and have different requirements regarding the types of outputs they expect. The technologies used to support Web application access are evolving along with the associated accessibility guidelines. We present a novel tool that aims to provide flexible and open support for addressing such issues. We describe the design of its main features including support for recent guidelines and tailored results presentations, and report on first technical and empirical validation s that have provided positive feedbackSource: Proceedings of the ACM on human-computer interaction 4 (2020). doi:10.1145/3397871
DOI: 10.1145/3397871
Metrics:
Broccia G., Manca M., Paternò F., Pulina F.
Automatic support for web accessibility validation needs to evolve for several reasons The increasingly recognised importance of accessibility implies that various stakeholders, with different expertise, look at it from different viewpoints and have different requirements regarding the types of outputs they expect. The technologies used to support Web application access are evolving along with the associated accessibility guidelines. We present a novel tool that aims to provide flexible and open support for addressing such issues. We describe the design of its main features including support for recent guidelines and tailored results presentations, and report on first technical and empirical validation s that have provided positive feedbackSource: Proceedings of the ACM on human-computer interaction 4 (2020). doi:10.1145/3397871
DOI: 10.1145/3397871
Metrics:
See at:
ISTI Repository | ISTI Repository | dl.acm.org 
| Proceedings of the ACM on Human-Computer Interaction | CNR ExploRA
2022
Journal article
Open Access
Empirical software engineering and formal methods for IoT systems
Basile D., Ter Beek M. H., Broccia G., Ferrari A.
Researchers from the Formal Methods and Tools (FMT) lab of ISTI-CNR are working on the application of formal methods to devise interaction protocols for safe-by-construction IoT Systems of Systems. They are also working on the empirical investigation and evaluation of the effectiveness of techniques and methodologies proposed for IoT application scenarios. The research is being conducted in the context of the national project T-LADIES, funded by the Italian Ministry of Education, University and Research (MIUR) under the program for Projects of National Interest (PRIN).Source: ERCIM news 131 (2022): 34–35.
Basile D., Ter Beek M. H., Broccia G., Ferrari A.
Researchers from the Formal Methods and Tools (FMT) lab of ISTI-CNR are working on the application of formal methods to devise interaction protocols for safe-by-construction IoT Systems of Systems. They are also working on the empirical investigation and evaluation of the effectiveness of techniques and methodologies proposed for IoT application scenarios. The research is being conducted in the context of the national project T-LADIES, funded by the Italian Ministry of Education, University and Research (MIUR) under the program for Projects of National Interest (PRIN).Source: ERCIM news 131 (2022): 34–35.
See at:
ercim-news.ercim.eu | 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
2020
Report
Open Access
Using spatial logic and model checking for nevus segmentation
Belmonte G., Broccia G., Ciancia V., Latella D., Massink M.
Spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems and signal and image analysis. In the latter domain, automatic and semi-automatic contouring in Medical Imaging has shown to be a very promising and versatile application that can greatly facilitate the work of professionals in this domain, while supporting explainability, easy replicability and exchange of medical image analysis methods. In recent work we have applied this model-checking technique to the (3D) contouring of tumours and related oedema in magnetic resonance images of the brain. In the current work we address the contouring of (2D) images of nevi. One of the challenges of treating nevi images is their considerable inhomogeneity in shape, colour, texture and size. To deal with this challenge we use a texture similarity operator, in combination with spatial logic operators. We apply our technique on images of a large public database and compare the results with associated ground truth segmentation provided by domain experts.Source: ISTI Technical Reports 2020/017, 2020
DOI: 10.32079/isti-tr-2020/017
Metrics:
Belmonte G., Broccia G., Ciancia V., Latella D., Massink M.
Spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems and signal and image analysis. In the latter domain, automatic and semi-automatic contouring in Medical Imaging has shown to be a very promising and versatile application that can greatly facilitate the work of professionals in this domain, while supporting explainability, easy replicability and exchange of medical image analysis methods. In recent work we have applied this model-checking technique to the (3D) contouring of tumours and related oedema in magnetic resonance images of the brain. In the current work we address the contouring of (2D) images of nevi. One of the challenges of treating nevi images is their considerable inhomogeneity in shape, colour, texture and size. To deal with this challenge we use a texture similarity operator, in combination with spatial logic operators. We apply our technique on images of a large public database and compare the results with associated ground truth segmentation provided by domain experts.Source: ISTI Technical Reports 2020/017, 2020
DOI: 10.32079/isti-tr-2020/017
Metrics:
See at:
ISTI Repository | CNR ExploRA
2021
Conference article
Open Access
Feasibility of Spatial Model Checking for Nevus Segmentation
Belmonte G., Broccia G., Ciancia V., Latella D., Massink M.
Recently developed spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems as well as signal and image analysis. In the latter domain, automatic and semi-automatic contouring in Medical Imaging has shown to be a very promising and versatile application that may facilitate the work of professionals in this domain, while supporting explainability, easy replicability and exchange of medical image analysis methods. In recent work, spatial model-checking has been applied to the 3D contouring of brain tumours and related oedema in magnetic resonance images of the brain. In the present paper we address the contouring of 2D images of nevi. One of the challenges of contouring nevi is that they show considerable inhomogeneity in shape, colour, texture and size. In addition these images often include also extraneous elements such as hairs, patches and rulers. To deal with this challenge we explore the use of a texture similarity operator in combination with spatial logic operators. We investigate the feasibility of our technique on images of a large public database. We compare the results with associated ground truth segmentation provided by domain experts; the results are very promising, both from the quality and from the performance point of view.Source: FormaliSE: International Conference on Formal Methods in Software Engineering, pp. 1–12, 18-21/05/2021
DOI: 10.1109/formalise52586.2021.00007
Metrics:
Belmonte G., Broccia G., Ciancia V., Latella D., Massink M.
Recently developed spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems as well as signal and image analysis. In the latter domain, automatic and semi-automatic contouring in Medical Imaging has shown to be a very promising and versatile application that may facilitate the work of professionals in this domain, while supporting explainability, easy replicability and exchange of medical image analysis methods. In recent work, spatial model-checking has been applied to the 3D contouring of brain tumours and related oedema in magnetic resonance images of the brain. In the present paper we address the contouring of 2D images of nevi. One of the challenges of contouring nevi is that they show considerable inhomogeneity in shape, colour, texture and size. In addition these images often include also extraneous elements such as hairs, patches and rulers. To deal with this challenge we explore the use of a texture similarity operator in combination with spatial logic operators. We investigate the feasibility of our technique on images of a large public database. We compare the results with associated ground truth segmentation provided by domain experts; the results are very promising, both from the quality and from the performance point of view.Source: FormaliSE: International Conference on Formal Methods in Software Engineering, pp. 1–12, 18-21/05/2021
DOI: 10.1109/formalise52586.2021.00007
Metrics:
See at:
ISTI Repository | www.computer.org | CNR ExploRA
2021
Report
Open Access
A graphical user interface for medical image analysis with declarative spatial logic - Cognitive and memory load evaluation
Broccia G., Ciancia V., Latella D., Massink M.
Logic based (semi-)automatic contouring in Medical Imaging has shown to be a very promising and versatile technique that can potentially greatly facilitate the work of different professionals in this domain while supporting explainability, easy replicability and exchange of medical image analysis methods. In such a context there is a clear need of a prototype Graphical User Interface (GUI) support for professionals which is usable, understandable and which reduces unnecessary cognitive load to the minimum, so that the focus of attention can remain on the main, critical, tasks such as image segmentation in support of planning of radiotherapy. In this paper we introduce a first proposal for a graphical user interface for the segmentation of medical images via the spatial logic based analyser VoxLogicA. Since both the logic approach to image analysis and its application in medical imaging are completely new, this is the first step in an iterative development process that will involve various analysis and development techniques, including empirical research and formal analysis. In the current work we analyse the GUI with a focus on the cognitive and memory load aspects which are critical in this domain of application.Source: ISTI Technical Report, ISTI-2021-TR/012, pp.1–39, 2021
DOI: 10.32079/isti-tr-2021/012
Metrics:
Broccia G., Ciancia V., Latella D., Massink M.
Logic based (semi-)automatic contouring in Medical Imaging has shown to be a very promising and versatile technique that can potentially greatly facilitate the work of different professionals in this domain while supporting explainability, easy replicability and exchange of medical image analysis methods. In such a context there is a clear need of a prototype Graphical User Interface (GUI) support for professionals which is usable, understandable and which reduces unnecessary cognitive load to the minimum, so that the focus of attention can remain on the main, critical, tasks such as image segmentation in support of planning of radiotherapy. In this paper we introduce a first proposal for a graphical user interface for the segmentation of medical images via the spatial logic based analyser VoxLogicA. Since both the logic approach to image analysis and its application in medical imaging are completely new, this is the first step in an iterative development process that will involve various analysis and development techniques, including empirical research and formal analysis. In the current work we analyse the GUI with a focus on the cognitive and memory load aspects which are critical in this domain of application.Source: ISTI Technical Report, ISTI-2021-TR/012, pp.1–39, 2021
DOI: 10.32079/isti-tr-2021/012
Metrics:
See at:
ISTI Repository | CNR ExploRA
2021
Conference article
Open Access
Querying medical imaging datasets using spatial logics (Position paper)
Belmonte G., Broccia G., Bussi L., Ciancia V., Latella D., Massink M.
Nowadays a plethora of health data is available for clinical and research usage. Such existing datasets can be augmented through artificial-intelligence-based methods by automatic, personalised annotations and recommendations. This huge amount of data lends itself to new usage scenarios outside the boundaries where it was created; just to give some examples: to aggregate data sources in order to make research work more relevant; to incorporate a diversity of datasets in training of Machine Learning algorithms; to support expert decisions in telemedicine. In such a context, there is a growing need for a paradigm shift towards means to interrogate medical databases in a semantically meaningful way, fulfilling privacy and legal requirements, and transparently with respect to ethical concerns. In the specific domain of Medical Imaging, in this paper we sketch a research plan devoted to the definition and implementation of query languages that can unambiguously express semantically rich queries on possibly multi-dimensional images, in a human-readable, expert-friendly and concise way. Our approach is based on querying images using Topological Spatial Logics, building upon a novel spatial model checker called VoxLogicA, to execute such queries in a fully automated way.Source: MEDI 2021 - Advances in Model and Data Engineering in the Digitalization Era, pp. 285–301, Tallinn, Estonia, 21-23/06/2021
DOI: 10.1007/978-3-030-87657-9_22
Metrics:
Belmonte G., Broccia G., Bussi L., Ciancia V., Latella D., Massink M.
Nowadays a plethora of health data is available for clinical and research usage. Such existing datasets can be augmented through artificial-intelligence-based methods by automatic, personalised annotations and recommendations. This huge amount of data lends itself to new usage scenarios outside the boundaries where it was created; just to give some examples: to aggregate data sources in order to make research work more relevant; to incorporate a diversity of datasets in training of Machine Learning algorithms; to support expert decisions in telemedicine. In such a context, there is a growing need for a paradigm shift towards means to interrogate medical databases in a semantically meaningful way, fulfilling privacy and legal requirements, and transparently with respect to ethical concerns. In the specific domain of Medical Imaging, in this paper we sketch a research plan devoted to the definition and implementation of query languages that can unambiguously express semantically rich queries on possibly multi-dimensional images, in a human-readable, expert-friendly and concise way. Our approach is based on querying images using Topological Spatial Logics, building upon a novel spatial model checker called VoxLogicA, to execute such queries in a fully automated way.Source: MEDI 2021 - Advances in Model and Data Engineering in the Digitalization Era, pp. 285–301, Tallinn, Estonia, 21-23/06/2021
DOI: 10.1007/978-3-030-87657-9_22
Metrics:
See at:
ISTI Repository | link.springer.com | link.springer.com | CNR ExploRA
2022
Contribution to conference
Open Access
Towards a GUI for declarative medical image analysis: cognitive and memory load issues
Broccia G., Ciancia V., Latella D., Massink M.
In medical imaging, (semi-)automatic image analysis techniques have been proposed to support the current time-consuming and cognitively demanding practice of manual segmentation of regions of interest (ROIs). The recently proposed image query language ImgQL, based on spatial logic and model checking, represents segmentation methods as concise, domain-oriented, human-readable procedures aimed at domain experts rather than technologists, and has been validated in several case studies. Such efforts are directed towards a human-centred Artificial Intelligence methodology. To this aim, we complemented the ongoing research line with a study of the Human-Computer Interaction aspects. In this work we investigate the design of a graphical user interface (GUI) prototype that supports the analysis procedure with minimal impact on the focus and the memory load of domain experts.Source: HCII 2022 - 24th International Conference on Human-Computer Interaction, pp. 103–111, Online conference, 26/06-01/07/2022
DOI: 10.1007/978-3-031-06388-6_14
Metrics:
Broccia G., Ciancia V., Latella D., Massink M.
In medical imaging, (semi-)automatic image analysis techniques have been proposed to support the current time-consuming and cognitively demanding practice of manual segmentation of regions of interest (ROIs). The recently proposed image query language ImgQL, based on spatial logic and model checking, represents segmentation methods as concise, domain-oriented, human-readable procedures aimed at domain experts rather than technologists, and has been validated in several case studies. Such efforts are directed towards a human-centred Artificial Intelligence methodology. To this aim, we complemented the ongoing research line with a study of the Human-Computer Interaction aspects. In this work we investigate the design of a graphical user interface (GUI) prototype that supports the analysis procedure with minimal impact on the focus and the memory load of domain experts.Source: HCII 2022 - 24th International Conference on Human-Computer Interaction, pp. 103–111, Online conference, 26/06-01/07/2022
DOI: 10.1007/978-3-031-06388-6_14
Metrics:
See at:
ISTI Repository | ISTI Repository | link.springer.com | 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