Extended Monitorability through Multiple Executions
Runtime Verification is a technique that uses monitors to analyse the execution of an executing system in order to determine whether a correctness property is satisfied or violated. Most of the work conducted thus far has been limited to the analysis of a single system execution for the verification of linear-time properties.
In this talk I will discuss recent work on investigating the increase in observational capabilities of monitors that analyse a system over multiple runs. I will illustrate how the augmented monitoring setup can affect the class of properties that can be verified at runtime, focussing instead on branching-time properties expressed in the modal mu-calculus. Although branching-time properties are considered by many to be the preserve of static verification techniques such as model-checking, our preliminary results show that the setup can be used to systematically extend previously established monitorability limits. If time permits, I will also discuss bounds that capture the correspondence between the syntactic structure of a branching-time property and the number of system runs required to conduct adequate runtime verification.
14/12/2023 14:00
Software Systems
Adrian Francalanza is a full professor at the University of Malta. His areas of expertise are static and runtime verification applied to behavioural models and languages for concurrency and distributed computation. He currently leads BehAPI: Behavioural APIs (https://www.um.edu.mt/projects/behapi/), an H2020 RISE project on behavioural theories for API-based software, and participates on a RANNIS project called MoVeMnt (http://icetcs.ru.is/movemnt/) which aims to extend the theory and capabilities of runtime verification.
