Parallel Runtime Monitoring
Runtime monitoring is a lightweight formal method used to check the correctness of software systems. The method deals with the runtime (or dynamic) behaviour of a system, usually by recording a sequence of events that happen when the system is run. The problem is then to check whether a temporal property holds for that behaviour. This can happen online, whilst the system is running, or offline, by inspecting a log file. Common specification languages for properties include temporal logic, automata, regular expressions and fixed-point logics. Runtime monitoring can be thought of as formal testing or single-run model checking.
Two major concerns with online runtime monitoring approaches are overhead and interference when monitoring a system whist it is running. One possible solution to this issue that has not received much attention so far is to utilise parallelism. This project will explore the current work in this area and develop new theoretical and practical techniques for parallel runtime monitoring. There exists both task-parallelism in the monitoring activity and data-parallelism in the program traces. Monitoring algorithms may be implemented as a stand-alone system or an extension of an existing runtime monitoring tool developed here at Manchester (either MarQ or RuleR). The project will offer the opportunity to enter the Runtime Verification competition and engage with our active international collaborations, including an ongoing collaboration with NASA JPL.
The interested student should have an interest in formal methods and program verification and have reasonable programming skills.