The RERS Grey Box Challenge 2012
Analysis of Event-Condition-Action Systems
(Event) Condition Action (ECA) System are omni-present in industrial practice. Programmable logical controllers (PLCs), user interfaces, and a lot of Web Services are essentially programmed this way. Moreover they underlie the more and more popular rule-based systems, which can be regarded as de-facto standards for dealing with permissions and access control, and they are promoted as a means for realizing compliant business processes on top of rule engines like Drools or jRules.
The popularity of this kind of programming comes from its apparent simplicity: one can add and change the functionality simply by adding and removing rules. What is difficult, however, is to understand and control the global implications of these apparently simple changes. Are there side-effects, is the new rule executed at all, does the whole rule system behave deterministically, does it terminate, etc..
In fact, treating ECA systems is very challenging for almost all verification and validation approaches, as there is little control structure to hook on to. The inherent structure of ECA systems (causalities, conflicts, dependencies,...) needs therefore to be inferred from their dataflow alone.
The RERS Grey Box Challenge at ISoLA 2012 invites everybody interested in the verification or validation of ECA systems to apply their techniques to the ECA setting. The aim is to reveal, compare and combine the specific strengths of the various validation techniques, be they manual, tool-supported or fully automated, for treating this peculiar but nevertheless practically highly important kind of systems.
In particular, during the challenge meeting at ISoLA 2012 it is planned to discuss the profile of the 2013 challenge held in November 2013 as satellite of ASE 2013 at NASA Ames in Moutain View. The third RERS challenge is planned to be part of ISoLA's 10th anniversary in 2014.
Characteristics of the Challenge
The challenge is very special in that it on the one hand is fully 'white-box': the full Java/C code will be available, but one the other hand has a black-box character: ECA code is particularly unstructured, not easy to analyze.
It will therefore be interesting to see how well e.g. program analysis techniques and model checking perform in comparison with black box techniques, and how these techniques may be profitably combined. We are therefore particularly looking forward to contributions based on tools that comprise one or the combination of many of the following technologies:
- program analysis and verification,
- symbolic execution,
- software model checking,
- statistcal model checking,
- model-based testing,
- inference of invariants,
- automata learning,
- run-time verification,
Of course, this list is not meant to be exhaustive. Rather we want to encourage everybody to approach this challenge with all the available means and ideas, and people are welcome to join effort and to approach the problem in heterogeneous teams.