Research
Research Focus
Formal Verification of Interactive Systems
We use state-based models and temporal logic to analyse the behaviour of safety-critical interactive systems. Model checking is applied to verify safety and usability properties, with counterexamples supporting the diagnosis of behavioural violations.
Safety-Critical User Interfaces Engineering
We study how methods for preventing use-related hazards can be integrated into human-centred design processes. Our work connects formal interaction models with concrete interface prototypes and analyses how interaction properties can be preserved and compared across interface variants in safety-critical contexts.
Model-Based Testing of User Interfaces
We derive systematic test strategies from task and behavioural models of interaction. This includes generating executable test sequences and incorporating potential use errors, so that testing addresses both intended use and plausible interaction deviations.
Usable Formal Methods
We investigate how formal verification can be made more understandable and usable in engineering practice. Our work includes generating natural-language explanations of model-checking counterexamples and deriving formal properties from structured natural-language requirements.
Selected projects
High-Assurance Medical Cyber-Physical Systems (NanoSTIMA RL 1.4)
Development of techniques to assess risk and to guarantee safe interaction with medical devices. (learn more)
OutSystems Learnability Model
We worked with OutSystems' UX experience group to improve the ease of adoption of their low-code development platform.
Languages and Tools for Critical Real Time Systems (BEST CASE RL8 )
Tools to ensure the safety and security of systems since the early stages of design. (learn more)
Pattern-based GUI Testing (PBGT)
Our role in the project was to develop a strategy for incorporating errors and plausible user behaviours into the test case generation process. (learn more)
Agile Prototyping for user Experience (APEX)
Development of a 3D Application Server-based rapid prototyping platform for ubiquitous computing environments. (learn more)
A model-based usability analysis environment (IVY)
Development of the IVY workbench for formal modelling and analysis of interactive systems. (learn more)