The RERS Challenge 2013
Co-located with ASE 2013, Silicon Valley, California, USA, November 11th -15th 2013
Rigorous Examination of Reactive Systems (RERS)
Reactive systems appear everywhere, e.g. as Web services, decision support systems, or logical controllers. Their validation techniques are as diverse as their appearance and structure. They comprise various forms of static analysis, model checking, symbolic execution and (model-based) testing, often tailored to quite extreme frame conditions. Thus it is almost impossible to compare these techniques, let alone to establish clear application profiles as a means for recommendation. The RERS Challenges aim at overcoming this situation by providing a forum for experimental profile evaluation based on specifically designed Benchmark suites. These benchmarks are automatically synthesized to exhibit chosen properties, and then enhanced to include dedicated dimensions of difficulty, ranging from conceptual complexity of the properties (e.g. reachablity, full safety, liveness), over size of the reactive systems (a few hundred lines to millions of them), to exploited language features (arrays and arithmatic at index pointer).
Characteristic for RERS is its wide scope, which addresses not only source code analyzers (White-Box problems), but also (model-based) testers and (test-based) modeler (Black-Box problems), and in particular Free stylers (Grey-Box problems). Currently, RERS focuses on functional properties only, but non-functional properties like time, performance, and stochastical behavior are envisaged. In addition, RERS 2013 will feature a number of case studies provided by industry.
A leading goal is to investigate the power of and synergy potential between source code-based (White-Box) approaches and purely testing-based (Black-Box) approaches:
- How much does the source code of historically grown legacy applications help?
- How far carries a purely testing-based investigation?
- What is a good way to combine the two?
Testing-based approaches are independent of language features, but, to quote Dijkstra, they can only proof the presence of errors, never their absence. Source code analysis has the power to proof the absence of errors, but each new language feature may requires an enormous effort. Realistic problems will most probably always require both approaches, which, today, are typically applied in isolation.
The RERS Challenge 2013 provides a wealth of problems of increasing complexity, the more involved of which will probably be beyond any individual state-of-the-art method or tool. In order to encourage cooperation and the consideration of alternative solutions RERS Challenges follows a clear free-style philosophy: apply whatever you have or you can get hold of, you are willing to specifically construct, and what you consider valuable.
This is also reflected in its evaluation: competitors will be offered 80+ benchmarks and asked to verify different properties of these benchmarks. In order to not impose/prefer any approach or technology the properties are reported as boolean answers to 12000+ queries on input/output behavior and reachability properties. A ranking of all handed in results determines the winner of the challenge in each category.
In addition there will be another 'ranking' based on the applied methodologies: papers describing the respective approaches are evaluated as scientific contributions. Detailed information can be found on the Rewards and Achievements page.
It is planned to publish an STTT Special Section on the RERS Challenge which summarizes the results and provides descriptions of the best solutions.