The RERS Challenge 2013 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. A large set of Benchmarks will be 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 (from a few hundred lines of code to millions of them), and
3. language features (arrays, indirect addressing, floating point arithmetics, virtual method calls, recursion).

Automaticall generated problems will be presented

• White-Box: i.e. in Java, C,
• Black-Box: as executables, not meant to be textually analyzed,
• Grey-Box: a mixture thereof.
  the problems have been replaced as of 9.9.2013, new deadline for the Grey Box part is 24.10.2013

Details about Benchmark generation can be found in this paper.

The challenge rules are essentially free style in order include as many participants as possible. They have a numeric part, which allows for a clear ranking in terms of number of correctly answered questions, and a textual part, where competitors are supposed to describe the approach. This part will be evaluated by the RERS committee. There are five price categories: White-Box, Black-Box, Grey-Box, overall and for the best approach taken (which must not necessarily have scored highest). In addition we will distribute achievement certificates for solutions passing a specific threshold.

Properties to analyze

For each of the systems, the contestants have to answer several questions, which can be divided into two classes:

• 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 IllegalStateException (Java) or a failed assertion (C), along with a specific error label.

• Behavioral properties:

  An execution trace of the ECA system consists of a sequence of inputs and outputs, each from a finite alphabet. Each system is dedicated to a file of properties, from which there exist 3 for the whole challenge. Each property file is designed for a different size of an input alphabet and 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).. The alphabet sizes in this challenge are of the sizes 6, 10 and 20 input symbols. 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.

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 may or may not 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 ECA program if and only if all possible runs which do not lead to an error satisfy the LTL property.