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.



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


The MarQ (Monitoring at Runtime with QEA) system, described in the TACAS 2015 paper above, is available at

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.


Those involved in this work include:

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.

Contact the Website Administrator with comments or queries about this website. All material copyright ©The University of Manchester. Last update 2013.