Runtime Verification and Specification Mining

Welcome to the Runtime Verification and Specification Mining Webpage

Runtime verification is the process of testing execution traces of computational systems against a description of one or more patterns of events that we wish to see satisfied by the traces. There are a number of approaches to this and considerable research activity in this area.

Specification mining is the process of examining execution traces of computational systems to determine patterns of event occurrences. These patterns are called "specifications" and indicate some aspects of the behaviour of the system. The examination of traces can occur at runtime or through post-run event logs.

We introduce Quantified Event Automata (QEAs) to provide a mechanism for specifying event patterns in traces. They allow us to consider data items in events and to quantify over the occurrence of such items in an execution trace. As automata, they give a computational as well as a logical aspect to the specifications.

We use QEAs as a basis for Runtime Verification and also as a means of Specification Mining where the specifications are, in fact, in the form of a QEA and they are mined using 'pattern-based' mining. In this we use a library of 'patterns', which again are in the form of QEAs, and, using runtime verification, establish which patterns hold in the traces and then combine these successful patterns to produce a specification.

Papers

• From First-order Temporal Logic to Parametric Trace Slicing. Giles Reger and David Rydeheard. The 15th International Conference on Runtime Verification (RV15), September 2015, Vienna.
• Suggesting Edits to Explain Failing Traces. Giles Reger. The 15th International Conference on Runtime Verification (RV15), September 2015, Vienna (Short Paper)
• MarQ: Monitoring at Runtime with QEA Giles Reger, Helena Cuenca Cruz and David Rydeheard. 21st International Conference on Tools and Analysis of Systems (TACAS) 2015. April, 2015, London. [Erratum: The automaton in Fig 1 should have a circular intitial state.]
• Automata-based Monitoring and Mining of Execution Traces University of Manchester PhD Thesis, Giles Reger. 2014.
• Automata-based Pattern Mining from Imperfect Traces. Giles Reger, Howard Barringer, and David Rydeheard. In Proceedings of the Second International Workshop on Software Mining. November 11-15, 2013. Silicon Valley, Calif. ASE 2013
• A Pattern-Based Approach to Parametric Specification Mining. Giles Reger, Howard Barringer, and David Rydeheard. In Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering (ASE 2013), Palo Alto, CA November 11-15, 2013. Acceptance rate: 23% (74/317).
• Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors. Howard Barringer, Yliés Falcone, Klaus Havelund, Giles Reger, and David Rydeheard. In Proceedings of the 18th International Symposium on Formal Methods (FM 2012), Paris, France, August 27-31, 2012. Springer 2012. Acceptance rate: 26% (35/132).
• Rule systems for run-time monitoring: from EAGLE to RULER. Howard Barringer, David Rydeheard, Klaus Havelund. Journal of Logic and Computation 20(3) 675-706, 2010.
• Runtime Verification of Log Files, A Trojan Horse for Formal Methods. H. Barringer, A. Groce, K. Havelund, D. Rydeheard, M.Smith. FMA 2009.
• A Pattern-Based Approach to Parametric Specification Mining. (Extended Version) Giles Reger, Howard Barringer, and David Rydeheard. Unpublished.

Competitions

Here are the results from the 2014 Runtime Verification Monitoring Competition, with the University of Manchester team as "QEA".

Code

The MarQ (Monitoring at Runtime with QEA) system, described in the TACAS 2015 paper above, is available at github.com/selig/qea.

Slides from talks

• The slides from a talk given at BCTCS 2013 giving an initial overview of our pattern-based approach to mining quantified event automata.
• The slides from the FM 2012 talk summarising quantified event automata.

Personnel

• Giles Reger
• Howard Barringer
• David Rydeheard
• Klaus Havelund
• Ylies Falcone

Related Work

Related to Runtime Verification is monitor-based evolution of computational systems, whereby systems are not only monitored for their conformance to a specification, but also, when conformance fails, systems can be modified via evolutionary changes. See the Evolvable Systems page for more details and a logical framework for describing such systems.