Minimum/maximum delay testing of product lines with unbounded parametric real-time constraints
Abstract Non-functional requirements like real-time behaviors are of ever-growing interest in many application domains of software product lines. Consequently, existing modeling formalisms and analysis techniques for reasoning about time-critical behaviors have to be adapted to product-line engineering, too. Featured timed automata (FTA) extend timed automata (TA) by feature constraints to enable efficient family-based verification of real-time properties. Here, we present configurable parametric timed automata (CoPTA) to further extend expressiveness of FTA by freely configurable and a-priori unbounded timing intervals of real-time constraints. Hence, CoPTA models impose infinite configuration spaces which makes variant-by-variant analysis practically infeasible. Instead, we present a family-based test-suite generation methodology for CoPTA models ensuring symbolical location coverage for every model configuration. Furthermore, we define a novel coverage criterion, called Minimum/Maximum Delay (M/MD) coverage, requiring every location in a CoPTA model to be reached by test cases with minimum/maximum possible durations, for systematically investigating best-case/worst-case execution times. We extend our family-based test-suite generation methodology to also achieve M/MD coverage on CoPTA models. Our evaluation results, obtained from applying our CoPTA tool to a collection of subject systems, reveal efficiency improvements of family-based test-suite generation, as compared to a variant-by-variant strategy in case of finite configuration spaces.