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 a user study on Attack-Defense Trees notation comprehensibility.
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).