Typology
operator:
and / or
Language
operator:
and / or
Date
operator:
and / or
Rights
operator:
and / or
2026
Contribution to book
Open Access
Formal methods for railway systems: a survey of research and technology transfer projects
Basile Davide, Ter Beek Maurice Henri, Broccia Giovanna, Gnesi Stefania, Mazzanti Franco, Spagnolo Giorgio Oronzo, Bacherini Stefano, Becheri Carlo, Grasso Daniele, Magnani Gianluca, Tempestini Matteo, Zingoni Niccolò, Ferrari Alessio
This paper offers a retrospective on collaborative projects that involved Alessandro Fantechi and the authors over the past two decades, from the shared perspective of the Formal Methods and Tools (FMT) lab of the Italian National Research Council (CNR) and former collaborators at General Electric (GE) Transportation and Alstom. The focus is on research and technology transfer efforts in the field of formal methods for railway systems, where Alessandro Fantechi’s contributions have been central to the development and application of formal specification, model-based verification, and tool-supported analysis. Joint work in projects such as ASTRail, 4SECURail, and TRACE-IT, as well as in industrial collaborations with Alstom and GE Transportation Systems illustrates the sustained impact of these activities on both academic research and industrial practice. This contribution reflects on the evolution of these efforts, the formal methods adopted, and the outcomes achieved in terms of methodologies, tools, and integration into safety-critical development processes. It also highlights the collaborative environment fostered across institutions and organizations, which has been instrumental in advancing the use of formal methods in the railway domain.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. 31-54
DOI: 10.1007/978-3-032-12484-5_3
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Basile Davide, Ter Beek Maurice Henri, Broccia Giovanna, Gnesi Stefania, Mazzanti Franco, Spagnolo Giorgio Oronzo, Bacherini Stefano, Becheri Carlo, Grasso Daniele, Magnani Gianluca, Tempestini Matteo, Zingoni Niccolò, Ferrari Alessio
This paper offers a retrospective on collaborative projects that involved Alessandro Fantechi and the authors over the past two decades, from the shared perspective of the Formal Methods and Tools (FMT) lab of the Italian National Research Council (CNR) and former collaborators at General Electric (GE) Transportation and Alstom. The focus is on research and technology transfer efforts in the field of formal methods for railway systems, where Alessandro Fantechi’s contributions have been central to the development and application of formal specification, model-based verification, and tool-supported analysis. Joint work in projects such as ASTRail, 4SECURail, and TRACE-IT, as well as in industrial collaborations with Alstom and GE Transportation Systems illustrates the sustained impact of these activities on both academic research and industrial practice. This contribution reflects on the evolution of these efforts, the formal methods adopted, and the outcomes achieved in terms of methodologies, tools, and integration into safety-critical development processes. It also highlights the collaborative environment fostered across institutions and organizations, which has been instrumental in advancing the use of formal methods in the railway domain.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. 31-54
DOI: 10.1007/978-3-032-12484-5_3
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
CNR IRIS 
| link.springer.com | CNR IRIS 
| CNR IRIS
2026
Conference article
Open Access
Fairness as a first-class requirement: a fairness hazard analysis approach to socio-technical processes
Broccia Giovanna, Lelii Lucio, Cirillo Roberto, Di Nucci Dario, Fricker Samuel, Palomba Fabio, Spagnolo Giorgio Oronzo, Ferrari Alessio
Context and Motivation. Fairness in socio-technical systems is increasingly recognised as a critical requirement, especially in processes involving human-AI interaction. Fairness hazards are situations or factors that threaten the fair treatment of individuals or groups. If left unaddressed, they can accumulate into systemic bias. Therefore, ensuring fairness must be treated as a first-class requirement during system design, rather than a post-hoc fix. Question/Problem. Systematic methods for identifying fairness hazards in socio-technical workflows and translating them into requirements-level mitigations are still missing. Principal Ideas/Results. We propose Fairness Hazard Analysis (FHA), an adaptation of hazard analysis methods from the safety-critical domain to analyse fairness in socio-technical processes. FHA is demonstrated through an AI-assisted hiring case and supported by HumAInFlow, a modelling and simulation platform. The approach is preliminarily evaluated through two focus groups. The feedback from participants highlights FHA’s usefulness for structured fairness analysis, the importance of diverse expertise, and the potential for deeper integration within HumAInFlow. Contribution. This work offers a novel method for integrating fairness into requirements analysis of socio-technical workflows, and provides an LLM-based tool to automate the analysis, marking a shift from bias detection to bias prevention with fairness-by-design.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16497, pp. 229-244. Poznań, Poland, 23–26 March 2026
DOI: 10.1007/978-3-032-21423-2_16
Metrics:
Broccia Giovanna, Lelii Lucio, Cirillo Roberto, Di Nucci Dario, Fricker Samuel, Palomba Fabio, Spagnolo Giorgio Oronzo, Ferrari Alessio
Context and Motivation. Fairness in socio-technical systems is increasingly recognised as a critical requirement, especially in processes involving human-AI interaction. Fairness hazards are situations or factors that threaten the fair treatment of individuals or groups. If left unaddressed, they can accumulate into systemic bias. Therefore, ensuring fairness must be treated as a first-class requirement during system design, rather than a post-hoc fix. Question/Problem. Systematic methods for identifying fairness hazards in socio-technical workflows and translating them into requirements-level mitigations are still missing. Principal Ideas/Results. We propose Fairness Hazard Analysis (FHA), an adaptation of hazard analysis methods from the safety-critical domain to analyse fairness in socio-technical processes. FHA is demonstrated through an AI-assisted hiring case and supported by HumAInFlow, a modelling and simulation platform. The approach is preliminarily evaluated through two focus groups. The feedback from participants highlights FHA’s usefulness for structured fairness analysis, the importance of diverse expertise, and the potential for deeper integration within HumAInFlow. Contribution. This work offers a novel method for integrating fairness into requirements analysis of socio-technical workflows, and provides an LLM-based tool to automate the analysis, marking a shift from bias detection to bias prevention with fairness-by-design.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16497, pp. 229-244. Poznań, Poland, 23–26 March 2026
DOI: 10.1007/978-3-032-21423-2_16
Metrics:
See at:
CNR IRIS | link.springer.com | doi.org | CNR IRIS | CNR IRIS
2025
Other
Open Access
HumAInFlow : a no-code platform for modelling and simulating Human-AI workflows
Broccia G., Cirillo R., Ferrari A., Lelii L., Spagnolo G. O.
The increasing integration of Generative AI (GenAI) agents into socio-technical systems, calls for platforms that can model, simulate, and analyse workflows involving both automated and human tasks. Existing agentic AI frameworks largely focus on automation and remain tightly bound to specific SDKs, often lacking structured support for human-in-the-loop modelling and simulation. To address these limitations, we introduce HumAInFlow, a no-code platform for modelling and simulating socio-technical workflows that explicitly integrates human roles as first-class nodes and supports their simulation via large language models (LLMs). The platform is SDK-agnostic, supports both local and remote LLM execution, and integrates the Model Context Protocol (MCP), ensuring interoperability and extensibility. Comparative analysis shows that HumAInFlow advances the state of the art by combining privacy-preserving deployment, execution monitoring, reproducibility, and explicit support for human–AI collaboration.DOI: 10.32079/isti-tr-2025/011
Metrics:
Broccia G., Cirillo R., Ferrari A., Lelii L., Spagnolo G. O.
The increasing integration of Generative AI (GenAI) agents into socio-technical systems, calls for platforms that can model, simulate, and analyse workflows involving both automated and human tasks. Existing agentic AI frameworks largely focus on automation and remain tightly bound to specific SDKs, often lacking structured support for human-in-the-loop modelling and simulation. To address these limitations, we introduce HumAInFlow, a no-code platform for modelling and simulating socio-technical workflows that explicitly integrates human roles as first-class nodes and supports their simulation via large language models (LLMs). The platform is SDK-agnostic, supports both local and remote LLM execution, and integrates the Model Context Protocol (MCP), ensuring interoperability and extensibility. Comparative analysis shows that HumAInFlow advances the state of the art by combining privacy-preserving deployment, execution monitoring, reproducibility, and explicit support for human–AI collaboration.DOI: 10.32079/isti-tr-2025/011
Metrics:
2025
Other
Open Access
ISTI-day 2025 Proceedings
Del Corso G., Pedrotti A., Federico G., Gennaro C., Carrara F., Amato G., Di Benedetto M., Gabrielli E., Belli D., Matrullo Zoe, Miori V., Tolomei Gabriele, Waheed T., Marchetti E., Calabrò Antonello., Rossetti G., Stella Massimo, Cazabet Rémy, Abramski K., Cau E., Citraro S., Failla A., Mesina V., Morini V., Pansanella V., Colantonio S., Germanese D., Pascali M. A., Bianchi L., Messina N., Falchi F., Barsellotti L., Pacini G., Cassese M., Puccetti G., Esuli A., Volpi L., Moreo Alejandro, Sebastiani F., Sperduti G., Nguyen Dong, Broccia G., Ter Beek M. H., Ferrari A., Massink M., Belmonte Gina, Ciancia V., Papini O., Canapa G., Catricalà B., Manca M., Paternò F., Santoro C., Zedda E., Gallo S., Maenza S., Mattioli A., Simeoli L., Rucci D., Carlini E., Dazzi P., Kavalionak H., Mordacchini M., Rulli C., Muntean Cristina Ioana, Nardini F. M., Perego R., Rocchietti G., Lettich F., Renso C., Pugliese C., Casini G., Haldimann Jonas, Meyer Thomas, Assante M., Candela L., Dell'Amico A., Frosini L., Mangiacrapa F., Oliviero A., Pagano P., Panichi G., Peccerillo B., Procaccini M., Mannocci A., Manghi P., Lonetti F., Kang Dongjae, Di Giandomenico F., Jee Eunkyoung, Lazzini G., Conti F., Scopigno R., D'Acunto M., Moroni D., Cafiso M., Paradisi P., Callieri M., Pavoni G., Corsini M., De Falco A., Sala F., Saraceni Q., Gattiglia Gabriele
ISTI-Day is an annual information and networking event organized by the Institute of Information Science and Technologies "A. Faedo" (ISTI) of the Italian National Research Council (CNR). This event features an opening talk of the Director of the Dept. DIITET (Emilio F. Campana) as well as an overview of the Institute's activities presented by the ISTI Director (Roberto Scopigno). Those institutional segments are complemented by dedicated presentations and round tables featuring former staff members, as well as internal and external collaborators. To foster a network of knowledge and collaboration among newcomers, the 2025 ISTI Day edition also includes a large poster session that provides a comprehensive overview of current research activities. Each of the 13 laboratories contributes 1–3 posters, highlighting the most innovative work and offering early-career researchers a platform for discussion. Thus these proceedings include the posters selected for ISTI-Day 2025, reflecting the diverse and innovative nature of the Institute's research.
Del Corso G., Pedrotti A., Federico G., Gennaro C., Carrara F., Amato G., Di Benedetto M., Gabrielli E., Belli D., Matrullo Zoe, Miori V., Tolomei Gabriele, Waheed T., Marchetti E., Calabrò Antonello., Rossetti G., Stella Massimo, Cazabet Rémy, Abramski K., Cau E., Citraro S., Failla A., Mesina V., Morini V., Pansanella V., Colantonio S., Germanese D., Pascali M. A., Bianchi L., Messina N., Falchi F., Barsellotti L., Pacini G., Cassese M., Puccetti G., Esuli A., Volpi L., Moreo Alejandro, Sebastiani F., Sperduti G., Nguyen Dong, Broccia G., Ter Beek M. H., Ferrari A., Massink M., Belmonte Gina, Ciancia V., Papini O., Canapa G., Catricalà B., Manca M., Paternò F., Santoro C., Zedda E., Gallo S., Maenza S., Mattioli A., Simeoli L., Rucci D., Carlini E., Dazzi P., Kavalionak H., Mordacchini M., Rulli C., Muntean Cristina Ioana, Nardini F. M., Perego R., Rocchietti G., Lettich F., Renso C., Pugliese C., Casini G., Haldimann Jonas, Meyer Thomas, Assante M., Candela L., Dell'Amico A., Frosini L., Mangiacrapa F., Oliviero A., Pagano P., Panichi G., Peccerillo B., Procaccini M., Mannocci A., Manghi P., Lonetti F., Kang Dongjae, Di Giandomenico F., Jee Eunkyoung, Lazzini G., Conti F., Scopigno R., D'Acunto M., Moroni D., Cafiso M., Paradisi P., Callieri M., Pavoni G., Corsini M., De Falco A., Sala F., Saraceni Q., Gattiglia Gabriele
ISTI-Day is an annual information and networking event organized by the Institute of Information Science and Technologies "A. Faedo" (ISTI) of the Italian National Research Council (CNR). This event features an opening talk of the Director of the Dept. DIITET (Emilio F. Campana) as well as an overview of the Institute's activities presented by the ISTI Director (Roberto Scopigno). Those institutional segments are complemented by dedicated presentations and round tables featuring former staff members, as well as internal and external collaborators. To foster a network of knowledge and collaboration among newcomers, the 2025 ISTI Day edition also includes a large poster session that provides a comprehensive overview of current research activities. Each of the 13 laboratories contributes 1–3 posters, highlighting the most innovative work and offering early-career researchers a platform for discussion. Thus these proceedings include the posters selected for ISTI-Day 2025, reflecting the diverse and innovative nature of the Institute's research.
See at:
CNR IRIS | www.isti.cnr.it | CNR IRIS
2025
Conference article
Open Access
An experience report on leveraging LLMs for GUI generation: automating coding to prioritise creativity
Broccia G., Borselli A., Cefaloni M. R., Delcorno F., Ferrari A.
The design of graphical user interfaces (GUIs) is a complex and time-consuming process that begins with identifying user roles and gathering requirements through interviews, surveys, or workshops. Designers then create low-fidelity sketches or digital wireframes, organising information into logical sections and selecting visual elements to enhance usability. This iterative process often demands extensive refinement based on stakeholder feedback, making mockup creation—especially for interactive prototypes—a time-consuming task. In particular, the mockup development process often entails spending significant effort on clerical activities, such as programming and debugging tasks, rather than concentrating on creativity, human interaction, and quick feedback cycles with stakeholders. This paper investigates whether large language models (LLMs) can assist GUI designers in streamlining the design process—reducing time and effort while maintaining design quality—enabling them to focus on the human aspects of creativity and user interaction by offloading technical programming tasks to the machine. We document our experience designing a dashboard for predictive maintenance in railways, illustrating how LLMs can support key tasks such as requirement analysis, information organisation, and mockup generation and refinement. We discuss insights and lessons learned, including the importance of clear requirements, the impact of LLM choice, and the benefits of iterative refinement in achieving stakeholder alignment. Our study shows that LLMs can support the GUI design process by automating specific tasks, thereby reducing design effort and enhancing the overall quality and satisfaction of the final product.
Broccia G., Borselli A., Cefaloni M. R., Delcorno F., Ferrari A.
The design of graphical user interfaces (GUIs) is a complex and time-consuming process that begins with identifying user roles and gathering requirements through interviews, surveys, or workshops. Designers then create low-fidelity sketches or digital wireframes, organising information into logical sections and selecting visual elements to enhance usability. This iterative process often demands extensive refinement based on stakeholder feedback, making mockup creation—especially for interactive prototypes—a time-consuming task. In particular, the mockup development process often entails spending significant effort on clerical activities, such as programming and debugging tasks, rather than concentrating on creativity, human interaction, and quick feedback cycles with stakeholders. This paper investigates whether large language models (LLMs) can assist GUI designers in streamlining the design process—reducing time and effort while maintaining design quality—enabling them to focus on the human aspects of creativity and user interaction by offloading technical programming tasks to the machine. We document our experience designing a dashboard for predictive maintenance in railways, illustrating how LLMs can support key tasks such as requirement analysis, information organisation, and mockup generation and refinement. We discuss insights and lessons learned, including the importance of clear requirements, the impact of LLM choice, and the benefits of iterative refinement in achieving stakeholder alignment. Our study shows that LLMs can support the GUI design process by automating specific tasks, thereby reducing design effort and enhancing the overall quality and satisfaction of the final product.
See at:
creare.iese.de | CNR IRIS | CNR IRIS
2025
Conference article
Open Access
On the impact of requirements smells in prompts: the case of automated traceability
Vogelsang A., Korn A., Broccia G., Ferrari A., Fischbach J., Arora C.
Large language models (LLMs) are increasingly used to generate software artifacts, such as source code, tests, and trace links. Requirements play a central role in shaping the input prompts that guide LLMs, as they are often used as part of the prompts to synthesize the artifacts. However, the impact of requirements formulation on LLM performance remains unclear. In this paper, we investigate the role of requirements smells— indicators of potential issues like ambiguity and inconsistency— when used in prompts for LLMs. We conducted experiments using two LLMs focusing on automated trace link generation between requirements and code. Our results show mixed outcomes: while requirements smells had a small but significant effect when predicting whether a requirement was implemented in a piece of code (i.e., a trace link exists), no significant effect was observed when tracing the requirements with the associated lines of code. These findings suggest that requirements smells can affect LLM performance in certain SE tasks but may not uniformly impact all tasks. We highlight the need for further research to understand these nuances and propose future work toward developing guidelines for mitigating the negative effects of requirements smells in AI-driven SE processes.Source: PROCEEDINGS - INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, pp. 51-55. Ottawa, Canada, 27/04-03/05/2025
DOI: 10.1109/icse-nier66352.2025.00016
Metrics:
Vogelsang A., Korn A., Broccia G., Ferrari A., Fischbach J., Arora C.
Large language models (LLMs) are increasingly used to generate software artifacts, such as source code, tests, and trace links. Requirements play a central role in shaping the input prompts that guide LLMs, as they are often used as part of the prompts to synthesize the artifacts. However, the impact of requirements formulation on LLM performance remains unclear. In this paper, we investigate the role of requirements smells— indicators of potential issues like ambiguity and inconsistency— when used in prompts for LLMs. We conducted experiments using two LLMs focusing on automated trace link generation between requirements and code. Our results show mixed outcomes: while requirements smells had a small but significant effect when predicting whether a requirement was implemented in a piece of code (i.e., a trace link exists), no significant effect was observed when tracing the requirements with the associated lines of code. These findings suggest that requirements smells can affect LLM performance in certain SE tasks but may not uniformly impact all tasks. We highlight the need for further research to understand these nuances and propose future work toward developing guidelines for mitigating the negative effects of requirements smells in AI-driven SE processes.Source: PROCEEDINGS - INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, pp. 51-55. Ottawa, Canada, 27/04-03/05/2025
DOI: 10.1109/icse-nier66352.2025.00016
Metrics:
See at:
CNR IRIS | ieeexplore.ieee.org | CNR IRIS | CNR IRIS
2024
Conference article
Open Access
Assessing the understandability and acceptance of attack-defense trees for modelling security requirements
Broccia G., Ter Beek M. H., Lluch Lafuente A., Spoletini P., Ferrari A.
Context and Motivation Attack-Defense Trees (ADTs) are a graphical notation used to model and assess security requirements. ADTs are widely popular, as they can facilitate communication between differ-ent stakeholders involved in system security evaluation, and they are for-mal enough to be verified, e.g., with model checkers. Question/Problem While the quality of this notation has been primarily assessed quanti-tatively, its understandability has never been evaluated despite being mentioned as a key factor for its success. Principal idea/Results In this paper, we conduct an experiment with 25 human subjects to assess the understandability and user acceptance of the ADT notation. The study focuses on performance-based variables and perception-based variables, with the aim of evaluating the relationship between these measures and how they might impact the practical use of the notation. The results confirm a good level of understandability of ADTs. Participants consider them useful, and they show intention to use them. Contribution This is the first study empirically supporting the understandability of ADTs, thereby contributing to the theory of security requirements engineering.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14588, pp. 39-56. Winterthur, Switzerland, April 8–11, 2024
DOI: 10.1007/978-3-031-57327-9_3
DOI: 10.48550/arxiv.2404.06386
Project(s): CODECS
, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Broccia G., Ter Beek M. H., Lluch Lafuente A., Spoletini P., Ferrari A.
Context and Motivation Attack-Defense Trees (ADTs) are a graphical notation used to model and assess security requirements. ADTs are widely popular, as they can facilitate communication between differ-ent stakeholders involved in system security evaluation, and they are for-mal enough to be verified, e.g., with model checkers. Question/Problem While the quality of this notation has been primarily assessed quanti-tatively, its understandability has never been evaluated despite being mentioned as a key factor for its success. Principal idea/Results In this paper, we conduct an experiment with 25 human subjects to assess the understandability and user acceptance of the ADT notation. The study focuses on performance-based variables and perception-based variables, with the aim of evaluating the relationship between these measures and how they might impact the practical use of the notation. The results confirm a good level of understandability of ADTs. Participants consider them useful, and they show intention to use them. Contribution This is the first study empirically supporting the understandability of ADTs, thereby contributing to the theory of security requirements engineering.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14588, pp. 39-56. Winterthur, Switzerland, April 8–11, 2024
DOI: 10.1007/978-3-031-57327-9_3
DOI: 10.48550/arxiv.2404.06386
Project(s): CODECS
, Typeful Language Adaptation for Dynamic, Interacting and Evolving SystemsMetrics:
See at:
arXiv.org e-Print Archive | CNR IRIS | link.springer.com | doi.org | doi.org | IRIS Cnr | CNR IRIS | CNR IRIS | IRIS Cnr
2024
Journal article
Open Access
Evaluating the understandability and user acceptance of Attack-Defense Trees: original experiment and replication
Broccia G., Ter Beek M. H., Lluch Lafuente A., Spoletini P., Fantechi A., Ferrari A.
Context: Attack-Defense Trees (ADTs) are a graphical notation used to model and evaluate security requirements. ADTs are popular because they facilitate communication among different stakeholders involved in system security evaluation and are formal enough to be verified using methods like model checking. The understandability and user-friendliness of ADTs are claimed as key factors in their success, but these aspects, along with user acceptance, have not been evaluated empirically. Objectives: This paper presents an experiment with 25 subjects designed to assess the understandability and user acceptance of the ADT notation, along with an internal replication involving 49 subjects. Methods: The experiments adapt the Method Evaluation Model (MEM) to examine understandability variables (i.e., effectiveness and efficiency in using ADTs) and user acceptance variables (i.e., ease of use, usefulness, and intention to use). The MEM is also used to evaluate the relationships between these dimensions. In addition, a comparative analysis of the results of the two experiments is carried out. Results: With some minor differences, the outcomes of the two experiments are aligned. The results demonstrate that ADTs are well understood by participants, with values of understandability variables significantly above established thresholds. They are also highly appreciated, particularly for their ease of use. The results also show that users who are more effective in using the notation tend to evaluate it better in terms of usefulness. Conclusion: These studies provide empirical evidence supporting both the understandability and perceived acceptance of ADTs, thus encouraging further adoption of the notation in industrial contexts, and development of supporting tools.Source: INFORMATION AND SOFTWARE TECHNOLOGY, vol. 178
DOI: 10.1016/j.infsof.2024.107624
Project(s): CODECS, Secure Internet of Things – Risk analysis in design and operation, Security-by-Design in Digital Denmark, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Broccia G., Ter Beek M. H., Lluch Lafuente A., Spoletini P., Fantechi A., Ferrari A.
Context: Attack-Defense Trees (ADTs) are a graphical notation used to model and evaluate security requirements. ADTs are popular because they facilitate communication among different stakeholders involved in system security evaluation and are formal enough to be verified using methods like model checking. The understandability and user-friendliness of ADTs are claimed as key factors in their success, but these aspects, along with user acceptance, have not been evaluated empirically. Objectives: This paper presents an experiment with 25 subjects designed to assess the understandability and user acceptance of the ADT notation, along with an internal replication involving 49 subjects. Methods: The experiments adapt the Method Evaluation Model (MEM) to examine understandability variables (i.e., effectiveness and efficiency in using ADTs) and user acceptance variables (i.e., ease of use, usefulness, and intention to use). The MEM is also used to evaluate the relationships between these dimensions. In addition, a comparative analysis of the results of the two experiments is carried out. Results: With some minor differences, the outcomes of the two experiments are aligned. The results demonstrate that ADTs are well understood by participants, with values of understandability variables significantly above established thresholds. They are also highly appreciated, particularly for their ease of use. The results also show that users who are more effective in using the notation tend to evaluate it better in terms of usefulness. Conclusion: These studies provide empirical evidence supporting both the understandability and perceived acceptance of ADTs, thus encouraging further adoption of the notation in industrial contexts, and development of supporting tools.Source: INFORMATION AND SOFTWARE TECHNOLOGY, vol. 178
DOI: 10.1016/j.infsof.2024.107624
Project(s): CODECS
, Secure Internet of Things – Risk analysis in design and operation, Security-by-Design in Digital Denmark, Typeful Language Adaptation for Dynamic, Interacting and Evolving SystemsMetrics:
See at:
Information and Software Technology | IRIS Cnr | IRIS Cnr | CNR IRIS
2023
Conference article
Open Access
Evaluating a language workbench: from working memory capacity to comprehension to acceptance
Broccia G, Ferrari A, Ter Beek Mh, 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.DOI: 10.1109/icpc58990.2023.00017
Project(s): Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Broccia G, Ferrari A, Ter Beek Mh, 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.DOI: 10.1109/icpc58990.2023.00017
Project(s): Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
See at:
CNR IRIS | ieeexplore.ieee.org | ISTI Repository | CNR IRIS | CNR IRIS
2023
Other
Restricted
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 - THE
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 - THE
2023
Book
Open Access
Message from the Chairs: FormaliSE 2023
Gnesi S, Plat N, Jakobs M C, Murray T, Ferrari A, Broccia G
This volume contains the papers presented at FormaliSE 2023: the 11th International Conference on Formal Methods in Software engineering, co-located with ICSE 2023, the 45th International Conference on Software Engineering.DOI: 10.1109/formalise58978.2023.00005
Metrics:
Gnesi S, Plat N, Jakobs M C, Murray T, Ferrari A, Broccia G
This volume contains the papers presented at FormaliSE 2023: the 11th International Conference on Formal Methods in Software engineering, co-located with ICSE 2023, the 45th International Conference on Software Engineering.DOI: 10.1109/formalise58978.2023.00005
Metrics:
See at:
CNR IRIS | ieeexplore.ieee.org | ISTI Repository | CNR IRIS
2023
Other
Open Access
D3.2.1: AA@THE User needs, technical requirements and specifications
Lorenza Pratali, Franca Delmastro, Mattia Campana, Flavio Di Martino, Loreto Pescosolido, Paolo Barsocchi, Giovanna Broccia, Vincenzo Ciancia, Claudio Gennaro, Michele Girolami, Gabriele Lagani, Diego Latella, Massimo Magrini, Marco Manca, Mieke Massink, Andrea Mattioli, Davide Moroni, Filippo Palumbo, Paolo Paradisi, Fabio Paternò, Laura Sebastiani, Claudio Vairo, Carmelina Santoro, Davide La Rosa
The objective of this deliverable is to compile a comprehensive report that describes the user needs, requirements, and technical specifications necessary to successfully implement the pilot study. To achieve this, it is crucial to establish contacts with specific associations and medical experts, which, collaboratively, will help to establish exclusion and inclusion criteria for the target population of healthy adults. Furthermore, another related objective is to define the different categories of users that will interact with the system and their specific needs. This holistic approach will ensure that the system is designed and developed to satisfy the diverse needs of the users and be aligned with the goals of the project. To achieve the milestone M3.2.1, we made significant progresses in the definition of the pilot study for the AA@THE subproject. One of our key achievements is the successful description of users’ needs, requirements, and technical specifications necessary for the study. We worked closely with both a specialized association of personal trainers for Adapted Physical Activity (APA) for older adults, already active in the area of Pisa, and the medical partner who played a crucial role in providing valuable insights and expertise to establish exclusion and inclusion criteria for the target population of healthy adults. In this milestone, we also defined the activities and services that we intend to offer. Specifically, we plan to provide technological systems aimed at monitoring physical and cognitive training processes, as well as stability evaluations, by instrumenting a gym dedicated to active and healthy ageing, which is located within the CNR research area in Pisa. Additionally, we will conduct sleep, nutrition, and sedentary assessments at the volunteers' homes. Furthermore, we successfully defined the different user categories involved in the study. To facilitate the recruitment process and people engagement, on January 17th 2023, we organized an open day in collaboration with the gym association where we presented the overall objectives of the project and we collected feedbacks from a group of healthy adults over 65, already involved in APA training. This allowed us to gain a comprehensive understanding of the users' specific needs in terms of system interactions, thus establishing the system requirements and technical specifications of the AA@THE ecosystem. In parallel, a specific action on “Automatic Support of Medical Image Analysis” has been initiated by members of the “Formal Methods and Tools” group at CNR-ISTI. Such an action aims at leveraging Formal Methods in Computer Science, Logic and Model Checking to augment state-of-the-art machine learning techniques for automatic medical image analysis, enabling end-users to make specific assumptions on the level of accountability and affordability of the system. The methodology is based on a strict intertwining between theory and experimentation, with the development of new theoretical foundations for model reduction and efficient model checking, and experimentation and finalization of a graphical user interface that is being evaluated from the points of view of usability and of cognitive load. Moreover, the design and implementation of a suitable GUI able to support the analysis of medical images has been conducted and tested with small groups of people derived from the hospital in Lucca. The proposed GUI prototype has been evaluated from a cognitive point of view in order to allow easy employment with little training, for general practitioners and caregivers who may lack the technical skills required to use fully-fledged medical imaging programs.Project(s): Tuscany Health Ecosystem
Lorenza Pratali, Franca Delmastro, Mattia Campana, Flavio Di Martino, Loreto Pescosolido, Paolo Barsocchi, Giovanna Broccia, Vincenzo Ciancia, Claudio Gennaro, Michele Girolami, Gabriele Lagani, Diego Latella, Massimo Magrini, Marco Manca, Mieke Massink, Andrea Mattioli, Davide Moroni, Filippo Palumbo, Paolo Paradisi, Fabio Paternò, Laura Sebastiani, Claudio Vairo, Carmelina Santoro, Davide La Rosa
The objective of this deliverable is to compile a comprehensive report that describes the user needs, requirements, and technical specifications necessary to successfully implement the pilot study. To achieve this, it is crucial to establish contacts with specific associations and medical experts, which, collaboratively, will help to establish exclusion and inclusion criteria for the target population of healthy adults. Furthermore, another related objective is to define the different categories of users that will interact with the system and their specific needs. This holistic approach will ensure that the system is designed and developed to satisfy the diverse needs of the users and be aligned with the goals of the project. To achieve the milestone M3.2.1, we made significant progresses in the definition of the pilot study for the AA@THE subproject. One of our key achievements is the successful description of users’ needs, requirements, and technical specifications necessary for the study. We worked closely with both a specialized association of personal trainers for Adapted Physical Activity (APA) for older adults, already active in the area of Pisa, and the medical partner who played a crucial role in providing valuable insights and expertise to establish exclusion and inclusion criteria for the target population of healthy adults. In this milestone, we also defined the activities and services that we intend to offer. Specifically, we plan to provide technological systems aimed at monitoring physical and cognitive training processes, as well as stability evaluations, by instrumenting a gym dedicated to active and healthy ageing, which is located within the CNR research area in Pisa. Additionally, we will conduct sleep, nutrition, and sedentary assessments at the volunteers' homes. Furthermore, we successfully defined the different user categories involved in the study. To facilitate the recruitment process and people engagement, on January 17th 2023, we organized an open day in collaboration with the gym association where we presented the overall objectives of the project and we collected feedbacks from a group of healthy adults over 65, already involved in APA training. This allowed us to gain a comprehensive understanding of the users' specific needs in terms of system interactions, thus establishing the system requirements and technical specifications of the AA@THE ecosystem. In parallel, a specific action on “Automatic Support of Medical Image Analysis” has been initiated by members of the “Formal Methods and Tools” group at CNR-ISTI. Such an action aims at leveraging Formal Methods in Computer Science, Logic and Model Checking to augment state-of-the-art machine learning techniques for automatic medical image analysis, enabling end-users to make specific assumptions on the level of accountability and affordability of the system. The methodology is based on a strict intertwining between theory and experimentation, with the development of new theoretical foundations for model reduction and efficient model checking, and experimentation and finalization of a graphical user interface that is being evaluated from the points of view of usability and of cognitive load. Moreover, the design and implementation of a suitable GUI able to support the analysis of medical images has been conducted and tested with small groups of people derived from the hospital in Lucca. The proposed GUI prototype has been evaluated from a cognitive point of view in order to allow easy employment with little training, for general practitioners and caregivers who may lack the technical skills required to use fully-fledged medical imaging programs.Project(s): Tuscany Health Ecosystem
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: COMMUNICATIONS IN COMPUTER AND INFORMATION SCIENCE (PRINT), 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: COMMUNICATIONS IN COMPUTER AND INFORMATION SCIENCE (PRINT), pp. 103-111. Online conference, 26/06-01/07/2022
DOI: 10.1007/978-3-031-06388-6_14
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | ISTI Repository | CNR IRIS | CNR IRIS | CNR IRIS
2022
Journal article
Open Access
Empirical software engineering and formal methods for IoT systems
Basile D, Ter Beek Mh, 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, vol. 131, pp. 34-35
Project(s): Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Basile D, Ter Beek Mh, 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, vol. 131, pp. 34-35
Project(s): Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
See at:
ercim-news.ercim.eu | CNR IRIS | ISTI Repository | CNR IRIS
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.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.DOI: 10.1109/formalise52586.2021.00007
Metrics:
See at:
CNR IRIS | ISTI Repository | www.computer.org | CNR IRIS | CNR IRIS
2021
Other
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.DOI: https://doi.org/10.32079/isti-tr-2021/012
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.DOI: https://doi.org/10.32079/isti-tr-2021/012
DOI: 10.32079/isti-tr-2021/012
Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS
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.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.DOI: 10.1007/978-3-030-87657-9_22
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS | link.springer.com
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, vol. 4
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, vol. 4
DOI: 10.1145/3397871
Metrics:
See at:
dl.acm.org | CNR IRIS | ISTI Repository | ISTI Repository | Proceedings of the ACM on Human-Computer Interaction | CNR IRIS | CNR IRIS | CNR IRIS
2020
Other
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.DOI: https://doi.org/10.32079/isti-tr-2020/017
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.DOI: https://doi.org/10.32079/isti-tr-2020/017
DOI: 10.32079/isti-tr-2020/017
Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2019
Software
Metadata Only Access
MAUVE++
Manca M, Paternò F, Santoro C, Iannuzzi N, Broccia G, Pulina F
3755 Registered users on 2023-05-24. 82817 Single pages have been evaluated since May the 10th 2021. 8924 Projects have been created since September the 29th 2019 for a total of 155506 validated pages.
Manca M, Paternò F, Santoro C, Iannuzzi N, Broccia G, Pulina F
3755 Registered users on 2023-05-24. 82817 Single pages have been evaluated since May the 10th 2021. 8924 Projects have been created since September the 29th 2019 for a total of 155506 validated pages.
See at:
CNR IRIS | mauve.isti.cnr.it