http://www.dagstuhl.de/17462

November 12 – 15 , 2017, Dagstuhl Seminar 17462

A Shared Challenge in Behavioural Specification

Organizers

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

For support, please contact

Susanne Bach-Bernhard for administrative matters

Andreas Dolzmann for scientific matters

Motivation

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.

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

Classification

  • Semantics / Formal Methods
  • Verification / Logic

Keywords

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

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.