Benchmarks

Different benchmarks have been used to assess performances and scalability of Static Verification in CLIMB (which is the most expensive supported verification).

Branching Responses

The first benchmark aims to evaluate the behaviour of SCIFF when detecting conflicts in a CLIMB model containing branching (OR) responses. More specifically, models have the following structure:

  • activity a1 must be performed at least once;
  • a1 is source of a branching response with two target activities, which in turn are sources of two branching responses with two target activities, and so on, until a “frontier” is reached;
  • each activity belonging to this “frontier” is attached to a negation precedence constraint pointing to a1 (which states that a1 must not be performed before), thus making the model inconsistent.

By increasing the number of activities/constraints, we notice that SCIFF scales very well: it is able to detect a conflict in a model containing 4095 activities in less than 2 minutes.

Alternate/Chain Responses with repeated executions

The two next benchmarks aim at evaluate SCIFF’s behaviour respectively in case of alternate and chain response constraints, especially when they are combined with existence constraints which impose more executions of the same activity:

  • the second (third resp.) benchmark impose at least N executions of an activity;
  • this activity is source of a sequence of K activities connected by alternate (chain resp.) response constraints;
  • the last activity of the sequence is subject to an absence formula which imposes at most N - 1 executions (the model is therefore inconsistent, because also such last activity should be performed at least N times)

Actually, discovering conflicts in alternate/chain response formulas when only one execution of the source activity is imposed reduces to the case of simple responses. This is attested also by SCIFF: on both benchmarks, when N = 1 presence of conflicts is detected almost immediately. When N increases, verification becomes more difficult. For alternate response constraints, this is due to the fact that more executions of the source activity trigger the interposition part of the formula, imposing and propagating a huge amount of temporal constrains. Note that, in case of simple DecSerFlow models (i.e., models which do not contain quantitative temporal constraints), chain constraints can be formalized in a simplified way, which leads to a dramatic speed-up of the verification: it answers in less than 10 sec. with K=15 and N=3.