• 10/04/15 Results up
  • 10/02/15 Solutions for challenge up
  • 09/05/15 RV traces and ext. file released
  • 08/26/15 Submission opened, RV dates updated
  • 07/18/15 RV training traces
  • 05/15/15 Training solutions up

Important Dates:

  • 05/15/15
       Solutions Training Phase
  • 08/01/15 - 09/04/15
       White Box Submission
  • 09/05/15
       Release Monitoring Input
  • 09/08/15
       RV Submission

Challenge Problem Description

The RERS Challenge 2015 will provide a wealth of benchmark problems of increasing complexity, the more involved of which will probably be beyond any individual state-of-the-art method or tool. The benchmarks are synthesized to exhibit chosen properties, and then enhanced in an automated process to cover dedicated dimensions of difficulty, including:

  1. conceptual complexity of the exhibited properties (reachability, safety, liveness),
  2. size of the systems in lines of code (from a few hundred lines to thousands of them) and size in terms of the state space to be explored, and
  3. language features (arrays, indirect addressing, floating point arithmetics, virtual method calls).

The problems are given in Java or C code for which the detailed syntax is explained on individual language pages:

The challenge rules are essentially free style in order include as many participants as possible. Details on the generation process of the Java and C problems can be found in this paper.

Properties to analyze

For the White-Box problems both behavioral and reachability properties have to be considered, while for the Runtime Verfication problems only the LTL formula that can be violated by finite traces are relevant.

For the two classes of properties several questions have to be answered, depending on the problem as described above. They are described in detail in the following passages:

  • Reachability:

    Some assignments to internal state variables correspond to erroneous states, which cause the system to fail with a specific error code. Not all of those error states are reachable, and the goal is to check which of these states can in fact be reached (it is not expected to also provide a sequence of inputs reaching them). Those errors come in the form of either an uncaught IllegalStateException in Java or failed assertion in C which both terminate the program. The IllegalStateException comes with a specific error label that can be extracted from the exception. In C there is an error label followed by assert, which prints the error label on the error stream.

    Each error/exception/assertion label defines a reachability problem, which you can solve with the method of your choice. There are no limitations.

  • Behavioral properties:

    An execution trace of a challenge system consists of a sequence of inputs and outputs, each from a finite alphabet. For each problem there exists a files with behavioral properties. It contains a set of 100 properties for which the contestants have to check whether they are satisfied by all traces, or if there are traces that violate them (it is not expected to also provide these traces).

    Some problems are provided with plain numbers as input and output symbols instead of strings which are used to specify the LTL formulae (an explicit request from participants). The translation is intuitive: "A" is 1, "B" is 2 etc. If violating traces are provided, please convert them to the string format.

    The properties are given both as an LTL formula and a textual description. For example,

        (G ! oU)
        output U does never occur

    states that it is not possible — by any sequence of input events — to make the system produce an "U" output action.

    In the LTL formulae, the atomic propositions correspond to input and output symbols, where the prefix i is used for input and o is used for output symbols, to allow a clear distinction.

    The LTL formulae are given in a standard syntax, making use of the following temporal operators:

    • X φ (next): φ has to hold after the next step
    • F φ (eventually): φ has to hold at some point in the future (or now)
    • G φ (globally): φ has to hold always (including now)
    • φ U ψ (until): φ has to hold until ψ holds (which eventually occurs)
    • φ WU ψ (weak until): φ has to hold until ψ holds (which does not necessarily occur)
    • φ R ψ (release): φ has to hold until ψ held in the previous step.

    Additionally, the boolean operators & (conjunction), | (disjunction) and ! (negation) are used.

    This properties, even if reminding of typical model checking problems, may also be dealt with in any fashion you like, e.g. data-flow analysis, symbolic execution, testing, learning, (statistical) model checking, run-time methods,....

Formal behavioral semantics

For evaluating the LTL formulae on the challenge problems, it is important to formally understand the behavioral semantics of the programs.

A program reads inputs (events) from the command line, and upon each event emit an output (for simplicity we restrict this to a finite set of outputs, of which at most one is issued before the next event occurs). Hence, an (infinite) run is an infinite word over a sequence of input and output symbols. The validity of an LTL formula over such a word is straightforward.

The LTL properties are intended to only specify the error-free behavior of the system. The rationale behind this is that it allows to formulate the specifications in a more compact way. For example, specifying that event A eventually leads to output Z being generated and interpreting it to hold for non-error runs only is probably more intuitive than specifying that A eventually leads to either Z or a fatal error.

Summing this up, an LTL property holds for a certain program if and only if all possible runs which do not lead to an error satisfy the LTL property. Additionally, the LTL formulae are only defined for the specified alphabet, inputs that are not in the alphabet are ignored by the program (no change of the internal state) and should not be considered for the evaluation of LTL properties.