TU Darmstadt / ULB / TUprints

Specification and Analysis of Software Systems with Configurable Real-Time Behavior

Luthmann, Lars (2020):
Specification and Analysis of Software Systems with Configurable Real-Time Behavior. (Publisher's Version)
Darmstadt, Technische Universität,
DOI: 10.25534/tuprints-00017363,
[Ph.D. Thesis]

[img]
Preview
Text
2020-12-14_Luthmann_Lars.pdf
Available under CC-BY 4.0 International - Creative Commons, Attribution.

Download (2MB) | Preview
Item Type: Ph.D. Thesis
Status: Publisher's Version
Title: Specification and Analysis of Software Systems with Configurable Real-Time Behavior
Language: English
Abstract:

Nowadays, non-functional properties and configurability are crucial aspects in the development of (safety-critical) software systems as software is often built in families and has to obey real-time requirements. For instance, industrial plants in Industry 4.0 applications rely on real-time restrictions to ensure an uninterrupted production workflow. Modeling these systems can be done based on well-known formalisms such as timed automata (TA). In terms of configurability, software product line engineering (SPLE) is used for developing variant-rich systems by integrating similar behavior into a product-line representation. In SPLE, we map core behavior and variable behavior to Boolean features representing high-level customization options, thus facilitating traceability between configuration models and behavioral models. However, only few formalisms combine real-time behavior with configurability. In particular, featured timed automata (FTA) support Boolean variability, whereas parametric timed automata (PTA) instead utilize numeric parameters, allowing us to describe infinitely many variants. Here, PTA facilitate an increased expressiveness as compared to FTA by using a-priori unbounded time intervals.

Unfortunately, there does not exist a formalism for real-time SPLs supporting traceability of Boolean features and infinitely many variants being available through parameters. Hence, we introduce configurable parametric timed automata (CoPTA), combining the advantages of Boolean features and numeric parameters. Therewith, we are able to model SPLs comprising an infinite number of variants while supporting traceability between configuration model and behavioral model.

For analyzing real-time properties of CoPTA, we cannot directly apply product-based approaches anymore due to the (possibly) infinite number of products. Hence, we develop quality-assurance techniques for CoPTA models. Here, sampling (i.e., the derivation of a subset of variants) still allows us to perform product-based analyses even in case of infinitely many products. To this end, we introduce a strategy specifically tailored to boundary cases of time-critical behavior.

Moreover, we introduce family-based techniques for quality assurance of CoPTA. For black-box analysis (where the behavioral model is unavailable), there already exist approaches for systematically reusing test cases among different configurations by accumulating configuration-specific information. However, these approaches only consider features, whereas we enhance these approaches by also considering parameters, allowing us to derive complete finite test suites satisfying product-based coverage criteria even in case of infinitely many variants. Additionally, our framework for test-case generation also covers boundary cases in terms of time-critical behavior. In case of white-box analysis, we introduce a formalism for a decidable check of timed bisimilarity, and we lift timed bisimulation to CoPTA.

We illustrate the concepts presented in this thesis by using a bench-scale demonstrator of an industrial plant as an example, and we evaluate our approaches based on a prototypical implementation, revealing efficiency improvements (in cases where we can compare our approach to other approaches) and applicability.

Alternative Abstract:
Alternative AbstractLanguage
Nichtfunktionale Eigenschaften und Konfigurierbarkeit sind wesentliche Aspekte bei der Software-Entwicklung, da Software häufig familienbasiert entwickelt wird und Echtzeitanforderungen hat. Beispielsweise haben Anwendungen im Bereich Industrie 4.0 Echtzeitbeschränkungen, um sicherzustellen, dass der Produktionsablauf nicht verzögert wird. Diese Systeme können dabei auf Basis bekannter Formalismen, wie z.B. Timed Automata (TA), modelliert werden. Im Bereich Konfigurierbarkeit ist Software Product Line Engineering (SPLE) ein wichtiger Aspekt für die Entwicklung variantenreicher Systeme, wobei ähnliches Verhalten in einer Produktlinie zusammengefasst wird. Im SPLE wird Kern- und variables Verhalten auf boolesche Features abgebildet, die Anpassungsoptionen darstellen und Artefakte aus Konfigurations- und Verhaltensmodell verknüpfen. Jedoch kombinieren nur wenige Formalismen beide Aspekte. Zum Beispiel unterstützen Featured Timed Automata (FTA) boolesche Variabilität, während Parametric Timed Automata (PTA) numerische Parameter verwenden, mit denen eine unendliche Anzahl von Varianten beschrieben werden kann. Hier bieten PTA durch die Nutzung von a priori unbegrenzten Zeitintervallen eine höhere Ausdrucksmächtigkeit als FTA. Bisher gibt es kein Modell für Echtzeitsysteme, das die Vorteile boolescher Variabilität und numerischer Parameter unterstützt. Daher führen wir Configurable Parametric Timed Automata (CoPTA) ein, die die Vorteile beider Ansätze kombinieren. Damit können wir Systeme modellieren, die unendlich viele Varianten umfassen und Artefakte aus dem Konfigurations- und Verhaltensmodell verknüpfen. Bei Nutzung von CoPTA können wir aufgrund der (potentiell) unendlichen Anzahl von Produkten keine produktbasierte Analyse mehr direkt anwenden, weshalb wir außerdem Techniken zur Qualitätssicherung von CoPTA vorstellen. Produktbasierte Ansätze können allerdings weiterhin unter Verwendung von Sampling durchgeführt werden. Jedoch existieren bisher keine Sampling-Strategien für unendliche Konfigurationsräume und Echtzeit-Produktlinien. Daher stellen wir eine Strategie vor, die das Extremverhalten von Echtzeitsystemen berücksichtigt. Des Weiteren stellen wir familienbasierte Techniken zur Qualitätssicherung von CoPTA vor. Im Bereich der Black-Box-Analyse (bei der das Verhaltensmodell nicht verfügbar ist) gibt es für das Testen bereits Ansätze zur Wiederverwendung von Testfällen zwischen Konfigurationen, welche jedoch nur boolesche Variabilität berücksichtigen. Deshalb erweitern wir diese Ansätze um Parameter, wodurch wir für CoPTA mit unendlich vielen Varianten vollständige Test-Suites ableiten können. Darüber hinaus deckt unsere Testfallgenerierung auch zeitkritisches Extremverhalten ab. Bei der White-Box-Analyse führen wir eine entscheidbare Überprüfung von TA-Bisimilarität ein und definieren Bisimulation für CoPTA. Wir veranschaulichen die in dieser Thesis vorgestellten Konzepte am Beispiel eines Demonstrators einer Industrieanlage und evaluieren unsere Ansätze anhand einer prototypischen Implementierung. Unsere Evaluationen zeigen dabei eine verbesserte Effizienz und generelle Anwendbarkeit unserer Ansätze.German
Place of Publication: Darmstadt
Collation: ix, 228 Seiten
Classification DDC: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Divisions: 18 Department of Electrical Engineering and Information Technology > Institute of Computer Engineering > Real-Time Systems
Date Deposited: 23 Dec 2020 08:25
Last Modified: 23 Dec 2020 21:14
DOI: 10.25534/tuprints-00017363
URN: urn:nbn:de:tuda-tuprints-173639
Referees: Schürr, Prof. Dr. Andy and Mousavi, Prof. Mohammad Reza and Lochau, Prof. Dr. Malte
Refereed: 2 December 2020
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/17363
Export:
Actions (login required)
View Item View Item