Tag: industry
Related publications: [SANER2019][RERS2019]
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.
The paper [SANER2019] describes a pilot study at ASML, investigating the learning time/completeness achieved trade-off of active learning. To resolve the trade-off the paper advocates extending active learning with execution logs and passive learning results. This extended approach is applied to components used in ASML TWINSCAN lithography machines. Compared to traditional active learning, this approach significantly reduces the active learning time. Moreover, it is capable of learning the behavior missed by the traditional active learning approach.
The Rigorous Examination of Reactive Systems (RERS) Challenge is an annual event concerned with software verification tasks—called benchmarks—on which participants can test the limits of their tools. In the 2019 edition of the RERS Challenge a new Industrial LTL/CTL/Reachability track is added, which contain programs that are based on real-world models of controller software provided by ASML.
For the RERS 2019 challenge, ASML disclosed anonymized information about the software of 33 TWINSCAN components. 3 components are used as practice problems and the remaining 30 components are used as challenge problems.
These components are Java/C programs which where generated from 33 models from 33 components used in ASML TWINSCAN machines as describe in the paper [SANER2019]. From a real-world ASML models as input the organizers generate interesting properties and an obfuscated software component. Details on parts of the generation process of the Java and C problems can be found in this [SPIN2013].
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.
For more details see RERS 2019's Industrial Problem Description and the [RERS2019] paper.
Download: challenge_and_training_set_with_dotfiles.zip.
This benchmark contains all these models in dot, aut, and nusmv format. Also the generated Java/C code from these models are included.
Finally also an execution log is provided for each model. 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
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.