12. – 15. November 2017, Dagstuhl Seminar 17462

A Shared Challenge in Behavioural Specification


Klaus Havelund (NASA – Pasadena, US)
Martin Leucker (Universität Lübeck, DE)
Giles Reger (University of Manchester, GB)
Volker Stolz (West. Norway Univ. of Applied Sciences – Bergen, NO)

Auskunft zu diesem Dagstuhl Seminar erteilt

Dagstuhl Service Team


Gemeinsame Dokumente
Programm des Dagstuhl Seminars [pdf]


Runtime verification (RV) as a field is broadly defined as focusing on processing execution traces (output of an observed system) for verification and validation purposes. Of particular interest is the problem of verifying that a sequence of events, a trace, satisfies a temporal property, formulated in a suitable formalism. Examples of such formalisms include state machines, regular expressions, temporal logics, context free grammars, variations of the mu-calculus, rule systems, stream processing systems, and process algebras. Of special interest is how to specify data rich systems, where events themselves carry data. Applications cover such domains as security monitoring and safety monitoring.

Such techniques are characterised by highly expressive languages for specifying behaviour, enabled by the concreteness of dealing directly with single runtime traces, which makes the verification problem tractable. However, this permitted expressiveness has also led to a divergence in such languages. The aim of this Dagstuhl Seminar is to shed light on the similarities and differences between these different formalisms, and specifically suggest directions for future collaboration and research. This effort can potentially lead to an attempt to standardize an RV formalism.

To achieve this, the main activity will be a challenge where participants are asked to specify a given set of behaviours in their own specification approach prior to the seminar. The challenge will allow for a diverse range of specification approaches, for example event vs time triggered, timed vs untimed, propositional vs parametric/firstorder, textual vs graphical, future-time vs past-time vs mixed, and alternative logics such as regular expressions, state machines, variants of temporal logic, etc. These solutions will then be presented, developed, and discussed during the seminar alongside other discussions relevant to the topic of behavioural specification languages. These discussions will allow input from various experts from inside and outside the community as well as from industry.

The seminar will include a mixture of tool developers, theoreticians and industry experts. Some of the issues that may be addressed by the seminar include:

  • Expressiveness of specification languages
  • Succinctness of specification languages
  • Usability of specification languages
  • Monitor input and output domains
  • Integration of instrumentation into specification languages
  • Tool support (textual vs. graphical editors, debugging support)

Additionally, we encourage participants to bring their own topics to discuss.

  Creative Commons BY 3.0 DE
  Klaus Havelund, Martin Leucker, Giles Reger, and Volker Stolz


  • Semantics / Formal Methods
  • Verification / Logic


  • Behavioural specification
  • Runtime verification
  • Temporal logic
  • Dynamic properties


Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.