I'm Giovanna Broccia, a post-doctoral fellow at the Formal Methods and Tools Laboratory of the Institute of Information Science and Technology (ISTI) of the National Research Council (CNR) in Pisa, Italy.

I received a PhD in Computer Science at the University of Pisa under the supervision of Prof. Paolo Milazzo. My PhD thesis A Formal Framework for Modelling and Analysing Safety-Critical Human Multitasking presents a formal model of safety-critical human multitasking which describes the cognitive processes involved in Human-Computer Interaction (HCI) and the switching of attention among concurrent tasks. The model builds on classical results from applied psychology on selective attention and working memory. The model has been implemented through a simulator, which gives quick feedback on whether a human can safely perform multiple tasks concurrently, and as an executable formal framework in Real-Time Maude, which allows analysing multitasking through reachability analysis and model checking. Finally, different case studies have been implemented and analysed.

During my PhD studies I spent 6 months abroad as a visiting researcher at the University of Oslo, the University of Minho, the École Polytechnique (Inria Saclay Île-De-France), and at the University of Edinburgh.

My research interests lie into different areas:

  • modelling, simulation, and verification of systems;
  • use of formal methods into different application domains such as HCI, medical imaging field, and cognitive science;
  • study of human aspects involved in software engineering such as usability, understandability and users' cognitive effort.

Some of my last works deal with the application of spatial model checking techniques to the analysis of medical images (see for instance this work ); the design, development and evaluation of a Graphical User Interface for the spatial model checker VoxLogicA (see for instance this work); and the design and creation of user studies on formal notations comprehensibility and acceptance (see for instance this work).

To foster my research results and to reach a broader audience, I like to produce videos and slides, that explain different aspects related to my research (see for instance some of my videos on medical imaging , the VoxLogicA input language, or the VoxLogicA usage).

Publications

  • Broccia, G., Ferrari, A., ter Beek, M., Cazzola, W., Favalli, L., Bertolotti, F. "Evaluating a Language Workbench: from Working Memory Capacity to Comprehension to Acceptance" International Conference on Program Comprehension (ICPC 2023), pp.54–58. IEEE (2023).
  • Broccia, G., Vincenzo, C., Latella, D., Massink, M. "Towards a GUI for Declarative Medical Image Analysis: Cognitive and Memory Load Issues" International Conference on Human-Computer Interaction (HCII 2022), pp.103–111. Springer, Cham (2022), (CCIS 1581).
  • Belmonte, G., Broccia, G., Bussi, L., Vincenzo, C., Latella, D., Massink, M. "Encoding and Verifying Guidelines for Automated Contouring in Radiotherapy using VoxLogicA" Ital-IA 2022 Convegno del Laboratorio Nazionale CINI-AIIS
  • Broccia G., Ciancia V., Latella D., Massink M. "A graphical user interface for medical image analysis with declarative spatial logic - Cognitive and memory load evaluation" ISTI Technical Report, ISTI-2021-TR/012, pp.1–39, 2021.
  • Belmonte, G., Broccia, G., Bussi, L., Ciancia, V., Latella, D., Massink, M. "Querying medical imaging datasets using spatial logics (position paper)" In: International Conference on Model and Data Engineering, pp. 285-301. Springer, Cham (2021, June).
  • Belmonte G., Broccia G., Ciancia V., Latella D., Massink M. "Feasibility of Spatial Model Checking for Nevus Segmentation" in 2021 IEEE/ACM 9th International Conference on Formal Methods in Software Engineering (FormaliSE), 2021, pp. 1-12
  • Belmonte G., Broccia G., Ciancia V., Latella D., Massink M. "Spatial Model Checking for Nevus Segmentation" in https://arxiv.org/abs/2012.13289
  • Broccia G., Manca M., Paternò F., Pulina F. "Flexible Automatic Support for Web Accessibility Validation“ in Proceedings of the ACM on Human-Computer Interaction, Volume 4 (EICS): 83:1-83:24 (2020)
  • G. Broccia, P. Milazzo, C. Belviso, C. Berrocal Montiel. "Validation of a Simulation Algorithm for Safety-Critical Human Multitasking" in Proceedings of 23rd International Symposium on Formal Methods, collocated workshop 8th International Symposium “From Data to Models and Back (DataMod)” (2019)
  • G. Broccia, P. Milazzo, P. C. Ölveczky. "Formal Modeling and Analysis of Safety-Critical Human Multitasking" in Innovations in Systems and Software Engineering, a NASA Journal
  • G. Broccia. "A Formal Framework for Modelling and Analysing Safety-Critical Human Multitasking" Ph.D. Thesis (2019), University of Pisa
  • G.Broccia, P. Masci, P. Milazzo. "Modeling and Analysis of Human Memory Load in Multitasking Scenarios: Late-Breaking Results" in Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2018): 9-15. ACM
  • G. Broccia, P. Milazzo, P. C. Ölveczky. "An Executable Formal Framework for Safety-Critical Human Multitasking" in NASA Formal Methods Symposium (NFM 2018): 54-69. Springer, Cham.
  • G. Broccia, P. Milazzo, P. C. Ölveczky. "An Algorithm for Simulating Human Selective Attention" in International Conference on Software Engineering and Formal Methods (SEFM 2017) : 48-55. Springer, Cham.
  • G. Broccia. "Model-Based Analysis of Driver Distraction by Infotainment Systems in Automotive Domain" in Proceedings of the 2017 ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2017): 133- 136
  • P. Milazzo, G. Pardini, G. Broccia. "Towards a High-Level Model Checking Language: Object-orientation, Data Structures and Local Variable Pruning" in International Workshop on Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems (FMICS-AVoCS 2016)

Activities

  • Reviewer for Software and Systems Modeling journal, PeerJ journal.
  • PC co-chair for the 9th, 10th, and 11th editions of the International Symposium "From Data to Models and Back (DataMod)" (DataMod2023, DataMod 2021, DataMod2020).
  • PC member of conferences and workshops in the field of formal methods (FormaliSE2024, iFM2022, CIFMA2019, DataMod2019, COSimCPS2019, COSimCPS2018).
  • Subreviewer for some of the top conferences in the field of formal methods and software engineering (iFM2023, ASE2023, FM2021, TACAS2021, SEFM2020).
  • Web & Social Media Chair for FormaliSE2023 and MUM2019.
  • Introductory lecture on Spatial logics and Spatio-temporal model checking on 3D MRI images and on the cognitive aspects involved in images analysis through VoxLogicA, at the Software Validation and Verification class (MSc computer science, Università di Pisa, 2021).
  • Co-supervisor for two Master Theses in Digital Humanities, Università di Pisa (Luca Vitrini and Stefano Costanzo, 2018).
  • Teaching Assistant at Java class (MSc Digital Humanities, Università di Pisa, 2016).
  • Designer of the logo for the FMT Lab.
  • Designer of the websites for DataMod2020, DataMod2021, DataMod2023, FormaliSE2023, and VoxLogicA.
  • Organizer of the first PhD Event at the University of Pisa (2019).
  • Ph.D. Students representative in the Ph.D. council (2017/2018).