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

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