Invited Talks


Testing automation using RoboStar

Ana Cavalcanti   – Professor at the University of York
York, United Kingdom

Ana Cavalcanti is a professor at the University of York and a Royal Academy of Engineering Chair in Emerging Technologies. She leads RoboStar, a centre of excellence on software engineering for robotics.


The RoboStar approach to model-based software engineering compliments the current practice of design and verification of mobile and autonomous robots, covering simulation, testing and proof. This approach is practical, supported by tools, and yet mathematically rigorous so that it can provide reliable evidence of trustworthiness.


Application of formal verification to the MAPE-K loop for self-adaptive systems

Cláudio Â. G. Gomes   – Assistant Professor at Aarhus University
Aarhus, Denmark

The performance and reliability of Cyber-Physical Systems are increasingly aided through the use of digital twins, which mirror the static and dynamic behaviour of a Cyber-Physical System (CPS) in software. Digital twins enable the development of self-adaptive CPSs which reconfigure their behaviour in response to novel environments. It is crucial that these self-adaptations are formally verified at runtime, to avoid expensive re-certification of the reconfigured CPS. In this talk, I discuss formally verified self-adaptation in a digital twinning system, by constructing a non-deterministic model which captures the uncertainties in the system behaviour after a self-adaptation. We use Signal Temporal Logic to specify the safety requirements the system must satisfy after reconfiguration and employ formal methods based on verified monitoring over Flow* flowpipes to check these properties at runtime. This gives us a framework to predictively detect and mitigate unsafe self-adaptations before they can lead to unsafe states in the physical system.


Claudio Gomes is currently an assistant professor at Aarhus University, working on engineering of digital twins, and the intersection between formal methods and self-adaptive systems. This section is focused on interdisciplinary research together with industry and they have several industrial case studies for which they are developing digital twins.