Hendrik Göttmann, Isabelle Bacher, Nicolas Gottwald, Malte Lochau

Dynamic Software Product Lines (DSPL) have recently gained momentum as integrated engineering methodology for (self-)adaptive software. DSPL enhance statically configurable software by enabling runtime reconfiguration to facilitate continuous adaptations to changing environmental contexts. In a previous work, we presented a model-based methodology for specifying and automatically analyzing real-time constraints of reconfiguration decisions in a feature-oriented and compositional way. Internally, we translate real-time-aware DSPL specifications into timed automata serving as input for off-the-shelf model-checkers like Uppaal for automatically checking semantic consistency properties. However, due to the very high computational complexity of model-checking timed automata, those consistency checks suffer from scalability problems thus obstructing practical applications of the proposed approach. In this paper, we tackle this issue by investigating various kinds of staticanalysis techniques that (1) aim to avoid expensive model-checker calls by statically detecting certain classes of inconsistencies beforehand and otherwise (2) perform model reduction by detecting and merging equivalence states prior to model-checker calls. The results of our experimental evaluation show very promising performance improvements achievable by those techniques, especially by the model-reduction approach.

We performed an experimental evaluation to illustrate the potential and feasibility of our approach. The central parts of our replication package can be found here:

In the following, we will explain how our experimental results can be reproduced. We presume that you have a machine that meets (at least) the following requirements:

• Desktop operating system based on Linux (64 bit)
• at least Java version 1.8 (or compatible)

As a first step, download the JAR and the archive containing the case studies into the same folder.
Next, extract the archive case-studies.zip. Thus, the folder case-studies will appear.
However, before you are able to run the tool you need to download Uppaal.

The tool requires Uppaal to function properly. To get Uppaal, follow these instructions:

1. You can get the academic version of Uppaal from here.
2. Download Uppaal 4.0 or higher (64 bit).
3. Open the folder and go to linux-bin.
4. In linux-bin, there is an executable file verifyta.
5. Copy the file verfifyta into the folder where you want to run the tool.

Now you can run the tool from the command line.
For instance, the following command runs a reachability analysis on the fifth case study:

java -jar rrcl-analyzer.jar -a r -n 6 case-studies/fm/fm0032.xml case-studies/rrcl/fm0032.rrcl

Besides the fm (.xml file) and the set of RRCL constraints (.rrcl file) the command contains two additional parameters.

• Parameter -a sets the type of the analysis.
  r corresponds to reachability, d to deadlock freedom, l to liveness, p to TA pattern and rrcl to the SAT-based analyses of the constraint set.
• Parameter -n sets the maximum number of constraints parsed from the RRCL file.
  If the file contains more lines than specified by parameter -n, then only the first n lines / constraints are taken into account.

Furthermore the tool supports the following parameter:

• Parameter -t sets a timeout in minutes.
  For instance, -t 30 interupts the execution of the tool after exceeding the limit of 30 minutes
• Parameter -j
  If set, evaluation results are written to the specified JSON file.
  Example usage: -j output.json

In case the papers is accepted to VaMoS'21 we will move this site with all supplementary data to https://zenodo.org/.
The corresponding URL in the paper will be adapted accordingly.