05 Fakultät Informatik, Elektrotechnik und Informationstechnik
Permanent URI for this collectionhttps://elib.uni-stuttgart.de/handle/11682/6
Browse
Search Results
Item Open Access Deriving bisimulation congruences in the DPO approach to graph rewriting. Long version(2004) Ehrig, Hartmut; König, BarbaraMotivated by recent work on the derivation of labelled transitions and bisimulation congruences from unlabelled reaction rules, we show how to solve this problem in the DPO (double-pushout) approach to graph rewriting. Unlike in previous approaches, we consider graphs as objects, instead of arrows, of the category under consideration. This allows us to present a very simple way of deriving labelled transitions (called rewriting steps with borrowed context) which smoothly integrates with the DPO approach, has a very constructive natureand requires only a minimum of category theory. The core part of this paper is the proof sketch that the bisimilarity based on rewriting with borrowed contexts is a congruence relation.Item Open Access Analysis and verification of systems with dynamically evolving structure(2004) König, Barbara; Esparza, Javier (Prof. Dr.)This thesis is concerned with verification and analysis techniques for software systems characterized by dynamically evolving structure, such as dynamic creation and deletion of objects, mobility and variable topology. Examples for such systems are pointer structures, object-based systems and communication protocols in which the number of participants is not constant. The approach taken here is based on graph transformation systems, an intuitive and---at the same time---powerful formalism for the modelling of distributed and mobile systems. So far there exists comparatively little research concerning the verification of graph rewriting. We will---in the first part of this thesis---introduce graph transformations and give an overview of existing analysis and verification methods, with a focus on the verification of systems with dynamically evolving structure. Then we will describe three original lines of research: behavioural equivalences, type systems and approximation by Petri nets, all of them concerned with the analysis of graph transformation systems. The second part consists of eight refereed research papers treating the previously introduced analysis and verification techniques in depth.Item Open Access Complexity results for checking distributed implementability(2004) Heljanko, Keijo; Stefanescu, AlinWe consider the distributed implementability problem as: Given a labelled transition system TS together with a distribution D of its actions over a set of processes, does there exist a distributed system over D such that its global transition system is equivalent' to TS? We consider the distributed system models of synchronous products of transition systems and Zielonka's asynchronous automata. In this paper we provide complexity bounds for the above problem with three interpretations of equivalent': as transition system isomorphism, as language equivalence, and as bisimilarity. In particular, we solve two problems left open in the literature. We also describe a logic programming implementation which complements the existing implementation for the synthesis of asynchronous automata initiated by the second author.Item Open Access A note on on-the-fly verification algorithms(2004) Schwoon, Stefan; Esparza, JavierThe automata-theoretic approach to verification of LTL relies on an algorithm for finding accepting cycles in the product of the system and a Büchi automaton for the negation of the formula. Explicit-state model checkers typically construct the product space "on the fly" and explore the states using depth-first search. We survey algorithms proposed for this purpose and propose two improved algorithms, one based on nested DFS, the other on strongly connected components. We compare these algorithms both theoretically and experimentally and determine cases where both algorithms can be useful.Item Open Access A case study : verifying a mutual exclusion protocol with process creation using graph transformation systems(2004) Dotti, Fernando Luis; König, Barbara; Santos, Osmar Marchi dos; Ribeiro, LeilaWe verify a mutual exclusion protocol with dynamic process creation based on token passing. The protocol is specified using object-based graph grammars. We introduce the protocol and show how the mutual exclusion property and other properties can be verified using the tool Augur, a verification tool for graph transformation systems based on an approximated unfolding technique.