This webpage provides an overview on our work concerning modeling and analysis of Configurable Parametric Timed Automata (CoPTA).

Directly go to Sampling Strategies for Product Lines with Unbounded Parametric Real-time Constraints – Replication Package

Directly go to Minimum/Maximum Delay Testing of Product Lines with Unbounded Parametric Real-Time Constraints – Replication Package

For our different approaches, we performed experimental evaluatiosn to illustrate the potential and feasability. The central parts of our replication packages can be found here:

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

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

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

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

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

In the following, we will explain the dependencies of our tool such that experimental results can be reproduced. Detailed instructions on how to use the tool are provided below in the sections for each paper. A detailed description of our benchmarking configuration can be found in the papers. 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, IMITATOR and the Z3 SMT solver 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 version 2.9.2, the tool needs to be built from scratch:

1. Visit the website and follow the simple instructions for "Installing IMITATOR from sources."
2. 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.

To get Z3 version 4.6.0, the library can be downloaded from GitHub:

1. Go to the website and navigate to release 4.6.0.
2. Extract the archive and go to the folder bin.
3. Move libz3 and libz3java to your java.library.path (e.g., /usr/lib)
4. Move com.microsoft.z3.jar to the folder CoPTA_lib (see the downloads in the Supplementary Data section in the beginning of this page).

The tool has a number of additional dependencies. Download the compressed libs folder and move them to the directory of the CoPTA jar file.

Lars Luthmann, Timo Gerecht and Malte Lochau

Combinatorial interaction testing (CIT) has been successfully applied to product-line testing for selecting from a usually very large configuration space a relatively small sample of test configurations sufficiently covering critical combinations of configuration options. As most recent CIT techniques like pairwise sampling are limited to finite configuration spaces (i.e., vectors of yes/no options), they are not directly applicable to configuration parameters with a-priori unbounded value domains (e.g., for adjusting unlimited resources or non-functional properties). Applying existing sampling strategies to infinite configuration spaces therefore requires further heuristics for selecting a finite subset of parameter-value combinations to be covered. Nevertheless, applying purely black-box heuristics may produce inherently ineffective test suites in which particularly critical parameter-value combinations are missed. To tackle this problem, we present a novel methodology for effectively sampling product lines with infinite configuration spaces by means of freely configurable real-time behaviors. To this end, we employ solution-space information obtained from our new modeling formalism, called configurable parametric timed automata (CoPTA), to generate samples for covering critical best-case/worst-case execution-time behaviors. We also present a tool implementation which we applied to a collection of subject systems to demonstrate applicability of our approach.

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.

java -jar CoPTA.jar -ptasampling \
-source CaseStudies/tgc_extended/Train-Gate-Controller.sc_p \
-fm CaseStudies/tgc_extended/tgc_extended_fm.xml -logLevel s

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

Real-time requirements are crucial in many modern application domains of software product lines. Hence, techniques for modeling and analyzing time-critical software have to be lifted to product-line engineering. Existing approaches extend timed automata by feature constraints to featured timed automata (FTA) facilitating efficient family-based verification of real-time properties. In this article, we propose configurable parametric timed automata (CoPTA), extending expressiveness of FTA by freely configurable and therefore a-priori unbounded timing intervals for real-time constraints, defined as feature attributes in extended feature models. The resulting infinite configuration spaces of CoPTA models make variant-by-variant analysis strategies infeasible. Thus, we present a family-based test-suite generation methodology for CoPTA models ensuring location coverage on every model configuration. Furthermore, we define a novel coverage criterion for time-critical product lines, Minimum/Maximum Delay (M/MD) coverage, requiring every location in a CoPTA model to be covered by test cases on those configurations having minimum/maximum possible durations for reaching the location, allowing us to investigate best-case/worst-case execution times. We extend the family-based test-suite generation methodology, to ensure M/MD coverage on a given CoPTA model. Finally, we present evaluation results from applying our CoPTA tool, demonstrating feasibility and efficiency improvements of family-based test generation, as compared to a variant-by-variant approach.

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. We also provide a log file for the outputs of our tool, running the complete evaluation of all case studies at once (link).

• 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 -pta -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 Best-Case Execution Times (FB-Min):

java -jar CoPTA.jar -ptamin -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 Worst-Case Execution Times (FB-Max):

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