Dr G Reger
Applications accepted all year round
Competition Funded PhD Project (Students Worldwide)
About the Project
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.
Funding Notes
This research project is one of a number of projects at this institution. It is in competition for funding with one or more of these projects. Usually the project which receives the best applicant will be awarded the funding. Applications for this project are welcome from suitably qualified candidates worldwide. Funding may only be available to a limited set of nationalities and you should read the full department and project details for further information.
References
Bartocci E., Falcone Y., Francalanza A., Reger G. (2018) Introduction to Runtime Verification. LNCS, vol 10457. https://link.springer.com/chapter/10.1007%2F978-3-319-75632-5_1
Medhat R., Bonakdarpour B., Fischmeister S., Joshi Y. (2016) Accelerated Runtime Verification of LTL Specifications with Counting Semantics. LNCS, vol 10012.https://link.springer.com/chapter/10.1007/978-3-319-46982-9_16/fulltext.html
Basin D., Caronni G., Ereth S., Harvan M., Klaedtke F., Mantel H. (2014) Scalable Offline Monitoring. LNCS, vol 8734.
https://link.springer.com/chapter/10.1007%2F978-3-319-11164-3_4
Continue with Facebook
