[TYPES/announce] Runtime Verification Benchmark Challenge 2018

[Giles Reger]

=====================================
Runtime Verification Benchmark Challenge 2018
=====================================
Key Dates
 - Submission deadline August 1st
 - RV Conference November 10-13
=====================================

We are pleased to announce the next iteration of the Runtime Verification Challenge. From 2014 to 2016 this ran as a competition comparing RV tools, principally on runtime performance, in three tracks based on the programming language of application. Following a hiatus in 2017 (holding the RV-CuBES workshop instead) we are announcing a more foundational RV Challenge for 2018. Modern software and cyber-physical systems require runtime verification, yet the burgeoning collection of RV technologies remain comparatively untested due to a dearth of benchmarks for objectively comparatively evaluating their performance. This is not for a lack of effort; it is due to a glaring gap in our understanding of what the benchmarks would need to look like, and of what exactly we need to measure. Therefore in 2018 we will host an RV Benchmark Competition to take the first major steps in filling this gap.

Entrants will be invited to submit benchmarks, where a benchmark consists of three parts as follows (more precise details will be given later in the formal rules of the competition):

1. Behaviour(s) produced by systems (e.g. traces). These may be provided directly as files or as generators producing such files (in which case some of the generated files will be included). Traces will be recorded as a set of finite sequences of pairs <value, time> with each sequence representing the behaviour from one source/variable and the pairs consisting of the value of that source and a timestamp.
2. A description of desired behaviour (specification). The main part of the competition will use a comparable core of basic MTL. While most RV tools reason over more expressive input languages, restriction to such a common fragment enables objective comparison of most RV tools.
3. An oracle i.e. the correct answer of whether the system/traces at a given time satisfy the specification. An oracle takes the same form as a behavior: it consists of a finite sequence of pairs <verdict, time> where verdict is a Boolean value stating whether the behavior(s) satisfy the specification at the given time.

All submissions (in the form of benchmarks or benchmark generators) will be submitted under an Open Data agreement. These will be collected in a public managed repository to enable broad access to the research community for evaluating RV methods, comparing the performance of RV tools, and forming the foundation for future RV tool competitions.

Submissions will be judged by an independent panel of experts (to be announced) and awards will be made in a number of categories (to be confirmed) such as key properties of the traces (e.g. length, diversity, complexity), the flexibility of the benchmark (e.g. are traces produced by a generator that can be parameterised), the complexity of the specification, the level of coverage of the specification by the traces (e.g. both positive and negative cases, other measures with good evidence), and other properties to be agreed by the panel after consultation with participants.

Benchmark submissions will be due August 1, 2018. Short papers describing the benchmarks/benchmark generators will be a maximum of 4 pages and due August 15, 2018. Entrants will be invited to present their submissions during the RV conference (https://rv2018.isp.uni-luebeck.de, November 10-13) at a special session.

To register your interest (and to receive further instructions necessary to take part) please fill in this form: https://goo.gl/forms/sI7Er22neA9TPtSx1

Further details will be provided on the competition website: https://www.rv-competition.org/2018-2/

Organisers:
Giles Reger, University of Manchester, UK
Volker Stolz, Western Norway University of Applied Sciences, Norway
Kristin Yvonne Rozier, Iowa State University, USA