Timed automata are a widely used formalism for specifying the discrete-state/continuous-time behavior of time-critical reactive systems. For the fundamental verification problem of comparing two timed automata, it has been shown that timed trace equivalence is undecidable, while timed bisimulation is decidable. The corresponding decidability proof uses region graphs, a finite but space-consuming characterization of timed automata semantics. Most verification tools use zone graphs instead, a symbolic and, on average, more space-efficient representation of timed automata semantics. However, zone graphs provide correct results only for those verification tasks that are reducible to reachability problems, and are too imprecise for timed bisimilarity checking. To the best of our knowledge, there is currently no practical tool for automated timed bisimilarity checking. In this paper, we propose a new representation of timed automata semantics that extends zone graphs by so-called virtual clocks. Our zone-based construction is, on average, significantly smaller than the corresponding region graph representation. We also present experimental results obtained by applying our tool implementation to timed automata models, which are often used to evaluate timed automata analysis techniques.

The management of modern enterprise applications is automated by coordinating the deployment, configuration, enactment, and termination of their components. Choosing among different candidate implementations for a specified application component requires such implementations to conform to the specified management behaviour. This holds especially if we wish to ensure that the overall application management can continue as planned, or that no additional (potentially undesired) management activity gets enabled. To this end, we introduce a formal framework for testing "management conformance", i.e., to test whether a candidate implementation can be managed according to the management protocol specifying the allowed management for a component. We also illustrate how our framework enables to run four different conformance tests, each providing a different trade-off between implementation freedom and guarantees on the overall application management. We formally prove that testing management conformance with constraints reducing implementation freedom results in preserving all already allowed management activities when implementing a specification by choosing a conforming implementation and that no additional (potentially undesired) management activity gets enabled. Finally, we assess our framework by means of a prototype implementation and its use in an experimental evaluation.

Modern enterprise applications integrate various heterogeneous components, which management has to be suitably coordinated. Being able to check whether the management allowed by the implementation of an application component conforms to a given specification hence becomes crucial. One may indeed wish to replace component specifications with conforming implementations, by ensuring that already planned management can be enacted, or that no additional (potentially undesired) management activities get enabled. In this perspective, we propose a parametric relation for testing the conformance of the management of application components, based on an existing formalism to model multi-component application management (i.e., management protocols). We also discuss how such relation can be exploited to ensure that replacing a specification with a conforming implementation continues to enable all already allowed management activities, and/or that no additional (potentially undesired) management activity gets enabled.

Recent research on quality assurance (QA) of configurable software systems (e.g., software product lines) proposes different analysis strategies to cope with the inherent complexity caused by the well-known combinatorial-explosion problem. Those strategies aim at improving efficiency of QA techniques like software testing as compared to brute-force configuration-by-configuration analysis. Sampling constitutes one of the most established strategies, defining criteria for selecting a drastically reduced, yet sufficiently diverse subset of software configurations considered during QA. However, finding generally accepted measures for assessing the impact of sample-based analysis on the effectiveness of QA techniques is still an open issue. We address this problem by lifting concepts from single-software mutation testing to configurable software. Our framework incorporates a rich collection of mutation operators for product lines implemented in C to measure mutation scores of samples, including a novel family-based technique for product-line mutation detection. Our experimental results gained from applying our tool implementation to a collection of subject systems confirms the widely-accepted assumption that pairwise sampling constitutes the most reasonable efficiency/effectiveness trade-off for sample-based product-line testing.

Dynamic Software Product Lines (DSPL) have recently shown promising potentials as integrated engineering methodology for (self-)adaptive software systems. Based on the software-configuration principles of software product lines, DSPL additionally foster reconfiguration capabilities to continuously adapt software products to ever-changing environmental contexts. However, in most recent works concerned with finding near-optimal reconfiguration decisions, real-time aspects of reconfiguration processes are usually out of scope. In this paper, we present a model-based methodology for specifying and automatically analyzing real-time constraints of reconfiguration decisions in a feature-oriented and compositional way. Those real-time aware DSPL specifications are internally translated into timed automata, a well-founded formalism for real-time behaviors. This representation allows for formally reasoning about consistency and worst-case/best-case execution-time behaviors of sequences of reconfiguration decisions. The technique is implemented in a prototype tool and experimentally evaluated with respect to a set of case studies 1 .

I/O conformance testing theories (e.g., ioco) are concerned with formally defining when observable output behaviors of an implementation conform to those permitted by a specification. Thereupon, several real-time extensions of ioco, usually called tioco, have been proposed, further taking into account permitted delays between actions. In this paper, we propose an improved version of tioco, called live timed ioco (ltioco), tackling various weaknesses of existing definitions. Here, a reasonable adaptation of quiescence (i.e., observable absence of any outputs) to real-time behaviors has to be done with care: ltioco therefore distinguishes safe outputs being allowed to happen, from live outputs being enforced to happen within a certain time period thus inducing two different facets of quiescence. Furthermore, tioco is frequently defined on Timed I/O Labeled Transition Systems (TIOLTS), a semantic model of Timed I/O Automata (TIOA) which is infinitely branching and thus infeasible for practical testing tools. Instead, we extend the theory of zone graphs to enable ltioco testing on a finite semantic model of TIOA. Finally, we investigate compositionality of ltioco with respect to parallel composition including a proper treatment of silent transitions.

Timed automata (TA) are a well-established formalism for specifying discrete-state/continuous-time behavior of time-critical reactive systems. Concerning the fundamental analysis problem of comparing a candidate implementation against a specification, both given as TA, it has been shown that timed trace equivalence is undecidable, whereas timed bisimulation equivalence is decidable. The corresponding proof utilizes region graphs, a finite, but generally very space-consuming characterization of TA semantics. Hence, most practical TA tools utilize zone graphs instead, a symbolic and generally more efficient representation of TA semantics, to automate analysis tasks. However, zone graphs only produce sound results for analysis tasks being reducible to plain reachability problems thus being too imprecise for checking timed bisimilarity. In this paper, we propose bounded zone-history graphs, a novel characterization of TA semantics facilitating an adjustable trade-off between precision and scalability of timed-bisimilarity checking. Our tool TimBrCheck is, to the best of our knowledge, the only currently available tool for effectively checking timed bisimilarity and even supports non-deterministic TA with silent moves. We further present experimental results gained from applying our tool to a collection of community benchmarks, providing insights into trade-offs between precision and efficiency, depending on the bound value.

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. In order 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, configurable parametric timed automata, 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 the applicability of our approach.

Featured transition systems (FTSs) and modal transition systems (MTSs) are two of the most prominent and well-studied formalisms for modeling and analyzing behavioral variability as apparent in software product line engineering. On one hand, it is well-known that for finite behavior FTSs are strictly more expressive than MTSs, essentially due to the inability of MTSs to express logically constrained behavioral variability such as persistently exclusive behaviors. On the other hand, MTSs enjoy many desirable formal properties such as compositionality of semantic refinement and parallel composition. In order to finally consolidate the two formalisms for variability modeling, we establish a rigorous connection between FTSs and MTSs by means of an encoding of one FTS into an equivalent set of multiple MTSs. To this end, we split the structure of an FTS into several MTSs whenever it is necessary to denote exclusive choices that are not expressible in a single MTS. Moreover, extra care is taken when dealing with infinite behavior: loops may have to be unrolled to accumulate FTS path constraints when encoding them into MTSs. We prove our encoding to be semantic-preserving (i.e., the resulting set of MTSs induces, up to bisimulation, the same set of derivable variants as their FTS counterpart) and to commute with modal refinement. We further give an algorithm to calculate a concise representation of a given FTS as a minimal set of MTSs. Finally, we present experimental results gained from applying a tool implementation of our approach to a collection of case studies.

We present a novel formal foundation for model-based testing of component-based software systems, unifying principles from modal interface theories and input/output conformance testing. Our theory relies on Modal Interface Automata with Input Refusals (IR-MIA) as behavioral formalism for both the specification and the implementation under test. IR-MIA models allow for a fine-grained distinction between mandatory and optional, as well as between underspecified and forbidden input/output behaviors, thus improving expressiveness of existing approaches in various ways. The input/output conformance relation on IR-MIA, called modal-irioco, therefore supports positive and negative conformance testing with optimistic and pessimistic environmental assumptions and is preserved under modal refinement. Our theory further adapts a variety of different composition operators from interfaces theories to IR-MIA models, each enjoying—under moderate restrictions—desirable compositionality properties with respect to the modal-irioco relation. Those operators include interface conjunction for incrementally integrating multiple perspectives on the same component, as well as parallel composition with multi-cast and hiding for integrating multiple concurrently interacting components. Furthermore, a quotient operator on IR-MIA, serving as the inverse to parallel composition, facilitates decomposition of conformance testing, thus providing a solution to the unknown-component problem.

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 CoFTA 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. (C) 2018 Elsevier Inc. All rights reserved.

We propose an input/output conformance testing theory utilizing Modal Interface Automata with Input Refusals (IR-MIA) as novel behavioral formalism for both the specification and the implementation under test. A modal refinement relation on IR-MIA allows distinguishing between obligatory and allowed output behaviors, as well as between implicitly underspecified and explicitly forbidden input behaviors. The theory therefore supports positive and negative conformance testing with optimistic and pessimistic environmental assumptions. We further show that the resulting conformance relation on IR-MIA, called modal-irioco, enjoys many desirable properties concerning component-based behaviors. First, modal-irioco is preserved under modal refinement and constitutes a preorder under certain restrictions which can be ensured by a canonical input completion for IR-MIA. Second, under the same restrictions, modal-irioco is compositional with respect to parallel composition of IR-MIA with multi-cast and hiding. Finally, the quotient operator on IR-MIA, as the inverse to parallel composition, facilitates decompositionality in conformance testing to solve the unknown-component problem.

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.

We present an adaptation of input/output conformance (ioco) testing principles to families of similar implementation variants as appearing in product line engineering. Our proposed product line testing theory relies on Modal Interface Automata (MIA) as behavioral specification formalism. MIA enrich I/O-labeled transition systems with may/must modalities to distinguish mandatory from optional behavior, thus providing a semantic notion of intrinsic behavioral variability. In particular, MIA constitute a restricted, yet fully expressive subclass of I/O-labeled modal transition systems, guaranteeing desirable refinement and compositionality properties. The resulting modal-ioco relation defined on MIA is preserved under MIA refinement, which serves as variant derivation mechanism in our product line testing theory. As a result, modal-ioco is proven correct in the sense that it coincides with traditional ioco to hold for every derivable implementation variant. Based on this result, a family-based product line conformance testing framework can be established.

Timed automata (TA) constitute a mature formalism for discrete-state/continuous-time behavior of time-critical cyber-physical systems. Concerning the fundamental analysis problem of comparing a candidate implementation against a specification both given as TA, it has been shown that timed trace equivalence is undecidable, whereas timed bisimulation is decidable. However, the limited expressiveness of TA is a serious obstacle in practice such that many TA extensions have been proposed. For instance, parametric timed automata (PTA) incorporate parametric clock constraints with freely-adjustable time intervals thus generalizing the constant time bounds of TA. In this way, PTA constitute a promising theoretical foundation for re-engineering static real-time specifications, originally given as TA, in a generic and customizable way. In this paper, we provide, to the best of our knowledge, the first proposal for lifting the notion of timed bisimulation from TA to PTA. Unfortunately, as PTA are Turing-complete, most interesting semantic properties being decidable for TA (including timed bisimulation), become undecidable for PTA. To tackle this issue, we propose an over-approximation of PTA semantics in terms of plain TA semantics and investigate decidability properties of a promising sub-class of PTA, called L/U-PTA.