SPLC'17

Modeling and Testing Product Lines with Unbounded Parametric Real-Time Constraints – Replication Package

Lars Luthmann, Andreas Stephan, Johannes Bürdek, and Malte Lochau

Abstract

Real-time requirements are crucial for embedded software in many modern application domains of software product lines. Hence, techniques for modeling and analyzing time-critical software have to be lifted to software product line engineering, too. Existing approaches extend timed automata (TA) by feature constraints to so-called featured timed automata (FTA) facilitating efficient verification of real-time properties for entire product lines in a single run. In this paper, we propose a novel modeling formalism, called configurable parametric timed automata (CoPTA), extending expressiveness of FTA by supporting freely configurable and therefore a-priori unbounded timing intervals for real-time constraints, which are defined as feature attributes in extended feature models with potentially infinite configuration spaces. We further describe an efficient test-suite generation methodology for CoPTA models, achieving location coverage on every possible model configuration. Finally, we present evaluation results gained from applying our tool implementation to a collection of case studies, demonstrating efficiency improvements compared to a variant-by-variant analysis.

Supplementary Data

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

ArtifactDownload
Binary file of the implementationJAR-File
Archive with all case studiesArchive (compressed)
Table 1 from the paper (overview on case studies)PDF
Table 2 from the paper (aggregation of all results)PDF

Case Studies

Train-Gate-Controller (TGC)

The case study describes a simple level crossing. The model consists of three components. Those are the Train wanting to cross, the Gate which has to be closed when the train is crossing and a controller, which controls the gate and receives signals from the train.

Reference: Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi: Parametric Real-time Reasoning. ACM, 1993.

Extension: The Train-Gate-Controller from the case study has been extended by two features, fast and slow, such that it is possible to model fast and slow trains.

Figures: Feature Model, CoPTA

Models: Link

Extended Train-Gate-Controller (ETGC)

This case study is an extension of the simple Train-Gate-Controller described above.

Reference: Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi: Parametric Real-time Reasoning. ACM, 1993.

Extension: For this evaluation, the case study is extended by five features. There are fast and slow trains as in the simple Train-Gate-Controller, and additionally, there is the possibility to send the position of the train with GPS. Furthermore the model is extended so that the technology of the gate may be new or old.

Figures: Feature Model, Train, Gate, Controller

Models: Link

GearControl (GC)

The gear controller is a component of the control system operating in a modern vehicle. The models describe changing between gears. GearControl consists of components for clutch, engine, gear control, gear box, and an interface.

Reference: Magnus Lindahl, Paul Pettersson, and Wang Yi: Formal Design and Analysis of a Gear-Box Controller. Springer, 2001.

Extension: The case study has been extended by seven features. The features new and old indicate the state of the technology. Features sport and drive indicate the mode of the gear control (in sport mode, the change of the gear is faster). Additionally, there is the feature fastChange, resulting in even faster gear changes. Furthermore, there are features gearSix and gearSeven for indication of additional gears.

Figures: Feature Model, Gear Control, Clutch, Engine, GearBox, Interface

Models: Link

Collision-Avoidance-Protocol (CA)

This case study describes the communication between different users using an Ethernet-like medium. To avoid collisions between different communications, a master is introduced to control the communication. The model consists of three users, three slaves, a master, a medium, a timer, and a check.

Reference: Henrik E. Jensen, Kim G. Larsen, and Arne Skou: Modelling and Analysis of a Collision Avoidance Protocol using SPIN and UPPAAL. BRICS Report Series, 1996.

Extension: For this evaluation, the case study has been extended by seven features. Features fast and slow indicate the performance of the communication. The feature withTimeout describes whether there should be an error if a message was not successfully sent after a certain amount of time. The features data1 to data4 describe four possible different data types.

Figures: Feature Model, Master, Medium, Timer, Check, Slave 1, Slave 2, Slave 3, User 1, User 2, User 3

Models: Link

Audio-Video-Controller (AVC)

This case study describes a messaging protocol for the communication between audio/video components. For communication, there is a single bus such that message may collide. The case study consists of models for bus, detector, frame generator, observer, and sender.

Reference: Klaus Havelund, Arne Skou, Kim G. Larsen, and Kristian Lund: Formal Modeling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using Uppaal. Springer, 2001.

Extension: For this evaluation, the case study has been extended by nine features. Features fast and slow indicate the performance of the communication. Furthermore, there is a differentiation between message types. In addition, one may choose between different error modes, indicating the error handling.

Figures: Feature Model, Bus, Detector A, Frame Generator, Observer A, Sender

Models: Link

Reproducing the Results

In the following, we will explain how our experimental results can be reproduced. A detailed description of our benchmarking configuration can be found in the paper. We presume that you have a machine that meets (at least) the following requirements:

  • Desktop operating system based on Linux 3.x (64 bit)
  • OpenJDK 1.8 (or compatible)
  • 4 GiB of RAM

The tool requires Uppaal and Imitator as well as additional dependencies 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. Add the path to verfifyta to your path variable or copy the file into the folder where you want to run the tool.

To get Imitator, use the following instructions:

  1. Download the binary file for Imitator from here.
  2. Extract the archive.
  3. Add the path to the extracted archive to your path variable or copy the extracted archive into the folder where you want to run the tool.

The tool has a number of additional dependencies. Download the JAR files and move them into the folder where you want to run the tool.

In order to run the tool, you have attached the .sc_p file and the .xml file of the feature model (amongst others). The following is an example call for the simple Train-Gate-Controller. If you want to run the tool with other case studies, simply change the .sc_p file and the feature model.

  • Product-by-Product Test-Suite Generation (PbP):

java -jar CoPTA.jar -pbp -reuse -tabView \
-source casestudies/tgc_simple/train-gate-controller-simple.sc_p \
-fm casestudies/tgc_simple/tgc_simple_fm.xml -logLevel s

  • Family-based Test-Suite Generation for bounded CoPTA (FB-B):

java -jar CoPTA.jar -fb -reuse -tabView \
-source casestudies/tgc_simple/train-gate-controller-simple.sc_p \
-fm casestudies/tgc_simple/tgc_simple_fm.xml -logLevel s

  • Family-based Test-Suite Generation for unbounded CoPTA (FB-U):

java -jar CoPTA.jar -fb -reuse -tabView \
-source casestudies/tgc_simple/train-gate-controller-simple.sc_p \
-fm casestudies/tgc_simple/tgc_simple_fm.xml -logLevel s