Challenge Setup and Rules

Contestants will be confronted with nine categories of ECA systems, ranging from structurally simple and small to structurally complex and huge, as well as corresponding collections of properties to be checked against these systems, which fall into two categories:

  1. implicit ones, given by errors/exceptions/assertions. These properties are only implicitly given within the code and should be checked for reachbility. Each individual reachability problem is evaluated and ranked exactly in the same fashion as the explicit properties.
  2. explicit ones, described verbally and formalized in temporal logic.

In addition to the 9 problem classes (systems plus set of properties) already published, we will pose three more problem classes at the end of August, which should be treated just in the same way. One of the corresponding systems will actually be a well-known system (pattern), which we encourage you to recognize. The correct answer here will be rewarded with 20 points.

There will be two kinds of rankings:

  1. According to the percentage of correctly put properties. In order to express one’s confidence in the answers, one can weight each answer with a weight between 0 and 9. In case of a correct answer, the weight is added to the overall score of the contestant. Otherwise, twice the weight is deduced.
  2. According to the employed (combination of) methods. In this category, solutions will be reviewed and ranked by the Challenge Team. Due to the possible variety of methods there may be several winners in this category.

The Challenge will have two parts:

  1. An offline part, where the contestants have two months to analyze all the challenge problems, to prepare their results, and to submit their solutions no later than 30.09.2012.
  2. An online part during ISoLA, where the contest have to prepare their results between the opening on Sunday 17.10,2012 and the presentation session on Thursday (21.10.2012) morning.


For the winners of each of the two kinds of the competition explained above, Springer sponsors a 500 Euro gift certificate for Springer books.

The teams with the best solutions in their categories will be invited for a STTT Special Section summarizing the results of the challenge, and, in particular, presenting the most advanced solutions.