Updates

  • Feb. 01, 2019:
       Sequential and industrial
       challenge problems released
  • Feb. 01, 2019:
       Parallel challenge problems    will be released asap
  • Jan. 25, 2019:
       Training problems
       now available

Important Dates:

  • Apr. 06 – 7, 2019:
       RERS at TACAS'19
       (TOOLympics)
  • Mar. 22, 2019:
       Solution submission
  • Feb. 01, 2019:
       Release of challenge
       problems
  • Jan. 25, 2019:
       Training problems
       available

Industrial Problem Description

Origin

ASML is the world's leading provider of lithography systems for the semiconductor industry. Lithography systems are very complex high-tech systems that are designed to expose patterns on silicon wafers. This processing not only must be able to deliver exceptionally reliable results with an extremely high output on a 24-7 basis, it must do so while also being extremely precise. With patterns becoming smaller and smaller, ASML TWINSCAN lithography systems incorporate an increasing amount of control software to compensate for nano-scale physical effects.

For the RERS 2019 challenge, ASML discloses anonymized information about the software of 33 TWINSCAN components. 3 components are used as practice problems and the remaining 33 components are used as challenge problems. Using these components allows participants to apply their tools and techniques on components of industrial size and complexity, evaluating their real-world applicability and performance.


Reactive system

The ASML-based problems of the industrial tracks are given in Java or C99 code and are similar to those of the sequential tracks. Taking a real-world ASML model as input, we generate interesting properties and obfuscate the model based on property-preserving transformations. Details on parts of the generation process of the Java and C problems can be found in this paper. The detailed syntax of the code is explained on individual language pages:

The generated C and Java programs can output the statement "invalid input" in which case an error has occurred. In such a case, the valid execution of the system has ended after the "invalid input" statement. For convenience, instead of terminating, the program reverts back to the state prior to receiving the last input symbol before "invalid input" was outputted.

In addition to Java/C code, an execution log is provided for each problem. Each execution log contains a selected number of logged traces, provided by ASML, representing behavior exhibited by either a unit or integration test. The execution logs are provided in the Abbadingo format. The first line is a header line providing the number of traces and the number of symbols (both inputs and outputs). The remaining lines each specify one trace.

The format of these lines is: 'label length input_1 output_1 input_2 output_2 ... input_n output_n', where

  • 'label' is always '1' indicating that the trace is a positive trace (accepted by the component),
  • 'length' is the length of the trace (2*n), and
  • and 'input_1 output_1 input_2 output_2 ... input_n output_n' is the trace consisting of alternating input and output symbols ('n' times an input and output symbol).
The different parts on a line are separated by white space.

The training problems also include original reference models (.aut files) based on which these three programs were generated. Furthermore, an actual (not obfuscated) Java implementation provided by ASML is included for the training problems in order to give further context to RERS' industrial tracks.

The challenge rules are essentially free style in order include as many participants as possible.


Properties to analyze

Each industrial track has its own set of properties to be analyzed. They are described in detail in the following paragraphs:

  • Reachability:

    These properties are relevant with regard to the Reachability problems. 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). The errors are modeled in form of an external undefined function __VERIFIER_error(int) (Errors.__VERIFIER_error(int) for Java) whose semantic abruptly terminates the program. The passed integer refers to the number of the error that caused the termination. If you want to compile and execute the problems please check the Java and C99 code description.

    Each such __VERIFIER_error(int) defines a reachability problem, which you can solve with the method of your choice. There are no limitations.

  • LTL:

    These properties are relevant with regard to the LTL problems. An execution trace of a challenge system consists of an infinite sequence of inputs and outputs, each from a finite alphabet. Note that finite executions of the given reactive system have to be ignored during model checking.

    The input and output symbols alternate, i.e., the output produced in response to an input occurs at the point in time immediately succeeding the time of the input event.

    For example, given the formula (i U o3), the trace i, o1, i, o2, i, o3, ... does not satisfy the formula as i does not hold in the second step.

    For each problem, there exists a file with behavioral LTL properties. This file defines the input and output alphabet in its first few lines. It contains a set of 20 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.

    These 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,....

  • CTL:

    These properties are relevant with regard to the CTL problems. In contrast to the Industrial LTL track, CTL properties have to be checked on all branches of the given system, including those that end eventually. Whereas the LTL properties of RERS only constrain infinite traces, branches that lead to finite paths have to be considered for CTL properties.

    Syntax

    The syntax of CTL properties used within the RERS Challenge 2019 is defined by the following Backus-Naur form:

     f::= 'true' | 'false' | f '&' f | f '|' f | f '=>' f | f '<=>' f
    		| '[]' f | '<>' f | '['a']' f | '<'a'>' f
    		| 'A(' f 'U' f ')' | 'E(' f 'U' f ')'
    		| 'A(' f 'W' f ')' | 'E(' f 'W' f ')'
    		| 'AG' f | 'EG' f | 'AF' f | 'EF' f
    	
    where each occurrence of a represent any input or output symbol. Note that "invalid input" is equivalent to "error" as explained above.

    Semantics

    The corresponding semantics adhere to usual definitions and can mostly be found in textbooks or papers such as this one. The formula "[] f" replaces "AX f" and "<> f" replaces "EX f". U stands for "strong until" whereas W stands for "weak until".

    Note that the above syntax does not include individual atomic propositions: State predicates cannot be expressed using this definition. This matches the fact that we constrain the behavior of transition systems instead of Kripke structures.

    Instead, it is possible to express that a formula f has to hold on certain successor states: The formula "[a] f" is true in state s if all outgoing transitions of s labeled with a lead to states that satisfy the formula f. Similarly, the formula "<a> f" holds in state s if there exists an outgoing transition of s labeled with a whose target state satisfies formula f.