arXiv subjects

Lars Luthmann

Publications and source records attributed to Lars Luthmann.

5 recordsLinked to original sources

arXiv2024

Checking Timed Bisimilarity with Virtual Clocks

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.

cs.FL↗

arXiv2019

Checking Timed Bisimulation with Bounded Zone-History Graphs -- Technical Report

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.

cs.FL↗

arXiv2019

Compositional Liveness-Preserving Conformance Testing of Timed I/O Automata -- Technical Report

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.

cs.LO↗

arXiv2016

Compositionality, Decompositionality and Refinement in Input/Output Conformance Testing - Technical Report

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.

cs.LO↗

arXiv2015

Towards an I/O Conformance Testing Theory for Software Product Lines based on Modal Interface Automata

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.

cs.SE↗