Malte Lochau

Alexander Lieb, Hendrik Göttmann, Lars Luthmann et al.

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.

Alexander Lieb, Malte Lochau

Timed automata provide a modeling formalism for time-critical properties of reactive systems with discrete-state/continuous-time behaviors. To handle the infinite state space of timed automata, recent verification tools use zone graphs, a symbolic semantic model that guarantees sound results, at least for properties reducible to reachability problems. If we instead want to compare the behavior of two timed automata, checking for timed trace equivalence is undecidable. Fortunately, timed bisimulation equivalence is decidable, but currently available checks do not provide useful explanations of the results. To overcome this limitation, we use a recently proposed extension of zone graphs by so-called virtual clocks. The extension not only facilitates effective tool support for timed bisimilarity checking but also enables the derivation of useful explanations from the results. If timed bisimilarity holds, all witnesses derivable from the composed symbolic representation of both models are indeed valid for both models. If timed bisimilarity does not hold, we describe how to obtain counterexamples, making explicit the behavioral differences. These witnesses/counterexamples may serve as test cases in later stages of system refinement.

Joel Greenyer, Malte Lochau, Thomas Vogel

This report documents the program and results of the GI-Dagstuhl Seminar 19023 on Explainable Software for Cyber-Physical Systems (ES4CPS). The seminar was concerned with the challenge that for future Cyber-Physical Systems (CPS), it will become increasingly relevant to explain their behavior (past, current, and future behavior, why a certain action was taken, how a certain goal can be achieved, etc.) to users, engineers, and other stakeholders. In order to increase the explainability of CPS and their engineering tools, fundamental, interdisciplinary research is required; solutions from multiple disciplines within software engineering, systems engineering, and related fields have to be applied, combined, and researched further. The goal of this seminar was to serve as a starting point for an interdisciplinary coordination of research activities targeting ES4CPS and an incubator of a new research community around this topic.

Frederik Deckwerth, Géza Kulcsár, Malte Lochau et al.

Feature models are used to specify variability of user-configurable systems as appearing, e.g., in software product lines. Software product lines are supposed to be long-living and, therefore, have to continuously evolve over time to meet ever-changing requirements. Evolution imposes changes to feature models in terms of edit operations. Ensuring consistency of concurrent edits requires appropriate conflict detection techniques. However, recent approaches fail to handle crucial subtleties of extended feature models, namely constraints mixing feature-tree patterns with first-order logic formulas over non-Boolean feature attributes with potentially infinite value domains. In this paper, we propose a novel conflict detection approach based on symbolic graph transformation to facilitate concurrent edits on extended feature models. We describe extended feature models formally with symbolic graphs and edit operations with symbolic graph transformation rules combining graph patterns with first-order logic formulas. The approach is implemented by combining eMoflon with an SMT solver, and evaluated with respect to applicability.

Géza Kulcsár, Frederik Deckwerth, Malte Lochau et al.

In graph transformation, a conflict describes a situation where two alternative transformations cannot be arbitrarily serialized. When enriching graphs with attributes, existing conflict detection techniques typically report a conflict whenever at least one of two transformations manipulates a shared attribute. In this paper, we propose an improved, less conservative condition for static conflict detection of graph transformation with attributes by explicitly taking the semantics of the attribute operations into account. The proposed technique is based on symbolic graphs, which extend the traditional notion of graphs by logic formulas used for attribute handling. The approach is proven complete, i.e., any potential conflict is guaranteed to be detected.