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

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.