November 12 – 15 , 2017, Dagstuhl Seminar 17462
A Shared Challenge in Behavioural Specification
For support, please contact
Susanne Bach-Bernhard for administrative matters
Andreas Dolzmann for scientific matters
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 and Martin Leucker and Giles Reger and Volker Stolz
- Semantics / Formal Methods
- Verification / Logic
- Behavioural specification
- Runtime verification
- Temporal logic
- Dynamic properties