Dagstuhl Seminar 17462
A Shared Challenge in Behavioural Specification
( Nov 12 – Nov 15, 2017 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/17462
Organizers
- 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)
Contact
- Andreas Dolzmann (for scientific matters)
- Susanne Bach-Bernhard (for administrative matters)
Schedule
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
This seminar dealt with the issue of behavioural specification from the viewpoint of runtime verification. 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 was 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.
The seminar included a mixture of tool developers, theoreticians, and industry experts and the above aim was addressed by two main activities.
The first activity was that each tool developer was asked to produce a brief summary of their specification language in the form of a set of short examples. These were then presented as talks during the Seminar, alongside other general contributed talks on issues surrounding behavioural specification. The examples were uploaded to a shared repository (which will be available via runtime-verification.org) and eleven participants added their tool descriptions and examples to this repository, producing a lasting resource from the seminar.
The second activity was carried out through eight working groups formed during the Seminar to discuss topics raised by the talks. The results of this working groups are detailed in this report. We take this opportunity to detail the topics (in the form of questions) proposed during the seminar that were not chosen for discussion in working groups:
- Where should we get specifications from? This question addressed both the issue of designing specification languages that can be usable by engineers but also the trending topic of inferring specifications from various artifacts and how specification languages can support this.
- How can we measure specification quality? What is a good specification, or when is one specification better than another? This might be related to coverage of the system being specified, or might be about interpretability or some other measure of usability.
- How do we ensure our specification language is not broken? This question was inspired by the experience of one speaker with developing the industrial-strength PSL language and the issues surrounding getting it right.
- How can we balance different levels of abstraction (e.g. local and global behaviour) in a specification? It was noted that specification languages are often closely associated with specifications at a certain level of abstraction. Is this an inherent restriction or a positive feature? Should we build specification languages with a certain level of abstraction in mind?
- How do we unify the different uses of a specification? This was inspired by the observation that a specification may be used to explain behaviour, check behaviour, or synthesize behaviour, and different presentations may be preferred in these different contexts.
This seminar was the first time the runtime verification community has reflected on the broad issue of specification and has fed into further developments including new perspectives for the international runtime verification competition, a proposed shared challenge involving the NASA core flight system, and the first informal survey and categorisation of actively developed runtime verification tools.
Giles Reger, Klaus Havelund, Martin Leucker, and Volker Stolz
- Wolfgang Ahrendt (Chalmers University of Technology - Göteborg, SE) [dblp]
- Cyrille Artho (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
- Domenico Bianculli (University of Luxembourg, LU) [dblp]
- Borzoo Bonakdarpour (McMaster University - Hamilton, CA) [dblp]
- Stijn de Gouw (Open University - Heerlen, NL) [dblp]
- Cindy Eisner (IBM - Haifa, IL) [dblp]
- Bernd Finkbeiner (Universität des Saarlandes, DE) [dblp]
- Adrian Francalanza (University of Malta - Msida, MT) [dblp]
- Sylvain Hallé (University of Quebec at Chicoutimi, CA) [dblp]
- Martin Leucker (Universität Lübeck, DE) [dblp]
- Zhiming Liu (Southwest University - Chongqing, CN) [dblp]
- Keiko Nakata (SAP Innovation Center - Potsdam, DE) [dblp]
- Dejan Nickovic (AIT Austrian Institute of Technology - Wien, AT) [dblp]
- Gordon Pace (University of Malta - Msida, MT) [dblp]
- Nicolas Rapin (CEA - Gif sur Yvette, FR) [dblp]
- Giles Reger (University of Manchester, GB) [dblp]
- Kristin Yvonne Rozier (Iowa State University, US) [dblp]
- César Sánchez (IMDEA Software - Madrid, ES) [dblp]
- Torben Scheffel (Universität Lübeck, DE) [dblp]
- Gerardo Schneider (Chalmers University of Technology - Göteborg, SE) [dblp]
- Julien Signoles (CEA LIST - Gif-sur-Yvette, FR) [dblp]
- Volker Stolz (West. Norway Univ. of Applied Sciences - Bergen, NO) [dblp]
- Hazem Torfah (Universität des Saarlandes, DE) [dblp]
- Dmitriy Traytel (ETH Zürich, CH) [dblp]
- Nobuko Yoshida (Imperial College London, GB) [dblp]
Classification
- semantics / formal methods
- verification / logic
Keywords
- behavioural specification
- runtime verification
- temporal logic
- dynamic properties
