Communication protocols, a class of critical systems, play an important role in industry. These protocols are critical because the tolerance for faults in these systems is low and it is highly desirable that these systems work correctly. Therefore, an effective methodology for describing and verifying that these systems behave according to their specifications is vitally important. Model checking is a verification technique in which a mathematically precise model of the system, either concrete or with abstraction, is built and a specification of how the system should behave is given. Then the system is considered correct if its model satisfies its specification. However, due to their size and complexity, critical systems, such as communication systems, are notoriously resistant to formal modelling and verification. In this thesis, we propose using graph transformation systems (GTSs), a visual semantic modelling approach, to model the behaviour of dynamically evolving communication protocols. Then, we show how a GTS model can facilitate verification of invariant properties of potentially unbounded communication systems. Finally, due to the use of similar isomorphic components in communication systems, we show how to exploit symmetries of these dynamically evolving models described by GTSs, to reduce the size of the model under verification. We use graph transformation systems to provide an expressive and intuitive visual description of the system state as a graph and for the computations of the system as a finite set of rules that transform the state graphs. Our model is well-suited for describing the behaviour of individual components, error-free communication channels amongst the components, and dynamic component creation and elimination. Thus, the structure of the generated model closely resembles the way in which communication protocols are typically separated into three levels: the first describing local features or components, the second characterizing interactions among components, and the third showing the evolution of the component set. The graph transformation semantics follows this scheme, enabling a clean separation of concerns when describing a protocol. This separation of concerns is a necessity for formal analysis of system behaviour. We prove that the finite set of graph transformation rules that describe behaviour of the system can be used to perform verification for invariant properties of the system. We show that if a property is preserved by the finite set of transformation rules describing the system model, and if the initial state satisfies the property, then the property is an invariant of the system model. Therefore, our verification method may avoid the explicit analysis of the potentially enormous state space that the transformation rules encode. In this thesis, we also develop symmetry reduction techniques applicable to dynamically evolving GTS models. The necessity to extend the existing symmetry reduction techniques arises because these techniques are not applicable to dynamic models such as those described by GTSs, and, in addition, these existing techniques may offer only limited reduction to systems that are not fully symmetric. We present an algorithm for generating a symmetry-reduced quotient model directly from a set of graph transformation rules. The generated quotient model is bisimilar to the model under verification and may be exponentially smaller than that model.

Communication protocols, a class of critical systems, play an important role in industry. These protocols are critical because the tolerance for faults in these systems is low and it is highly desirable that these systems work correctly. Therefore, an effective methodology for describing and verifying that these systems behave according to their specifications is vitally important. Model checking is a verification technique in which a mathematically precise model of the system, either concrete or with abstraction, is built and a specification of how the system should behave is given. Then the system is considered correct if its model satisfies its specification. However, due to their size and complexity, critical systems, such as communication systems, are notoriously resistant to formal modelling and verification. In this thesis, we propose using graph transformation systems (GTSs), a visual semantic modelling approach, to model the behaviour of dynamically evolving communication protocols. Then, we show how a GTS model can facilitate verification of invariant properties of potentially unbounded communication systems. Finally, due to the use of similar isomorphic components in communication systems, we show how to exploit symmetries of these dynamically evolving models described by GTSs, to reduce the size of the model under verification. We use graph transformation systems to provide an expressive and intuitive visual description of the system state as a graph and for the computations of the system as a finite set of rules that transform the state graphs. Our model is well-suited for describing the behaviour of individual components, error-free communication channels amongst the components, and dynamic component creation and elimination. Thus, the structure of the generated model closely resembles the way in which communication protocols are typically separated into three levels: the first describing local features or components, the second characterizing interactions among components, and the third showing the evolution of the component set. The graph transformation semantics follows this scheme, enabling a clean separation of concerns when describing a protocol. This separation of concerns is a necessity for formal analysis of system behaviour. We prove that the finite set of graph transformation rules that describe behaviour of the system can be used to perform verification for invariant properties of the system. We show that if a property is preserved by the finite set of transformation rules describing the system model, and if the initial state satisfies the property, then the property is an invariant of the system model. Therefore, our verification method may avoid the explicit analysis of the potentially enormous state space that the transformation rules encode. In this thesis, we also develop symmetry reduction techniques applicable to dynamically evolving GTS models. The necessity to extend the existing symmetry reduction techniques arises because these techniques are not applicable to dynamic models such as those described by GTSs, and, in addition, these existing techniques may offer only limited reduction to systems that are not fully symmetric. We present an algorithm for generating a symmetry-reduced quotient model directly from a set of graph transformation rules. The generated quotient model is bisimilar to the model under verification and may be exponentially smaller than that model.

<p>Correct certificate revocation practices are essential to each public-key infrastructure. While there exist a number of protocols to achieve revocation in PKI systems, there has been very little work on the theory behind it: Which different types of revocation can be identified? What is the intended effect of a specific revocation type to the knowledge base of each entity?</p><p>As a first step towards a methodology for the development of reliable models, we present a graph-based formalism for specification and reasoning about the distribution and revocation of public keys and certificates. The model is an abstract generalization of existing PKIs and distributed in nature; each entity can issue certificates for public keys that they have confidence in, and distribute or revoke these to and from other entities.</p><p>Each entity has its own public-key base and can derive new knowledge by combining this knowledge with certificates signed with known keys. Each statement that is deduced or quoted within the system derives its support from original knowledge formed outside the system. When such original knowledge is removed, all statements that depended upon it are removed as well. Cyclic support is avoided through the use of support sets.</p><p>We define different revocation reasons and show how they can be modelled as specific actions. Revocation by removal, by inactivation, and by negation are all included. By policy, negative statements are the strongest, and positive are the weakest. Collisions are avoided by removing the weaker statement and, when necessary, its support.</p><p>Graph transformation rules are the chosen formalism. Rules are either interactive changes that can be applied by entities, or automatically applied deductions that keep the system sound and complete after the application of an interactive rule.</p><p>We show that the proposed model is sound and complete with respect to our definition of a valid state.</p> / Report code: LIU-TEK-LIC-2006:1

While aspect-oriented programming (AOP) addresses the introduction of “aspects” at the code level, we argue that addressing this at the level of software architecture is conceptually and methodologically more adequate, since many aspects, that is, “crosscutting concerns”, are formulated already in the requirements, and therefore can be dealt with in a more controlled manner in the “earlier” phase of software architecture design. We use the precise concept of software architectures organised as diagrams over a category of component specifications, where the architecture semantics are defined as a colimit specification (Fiadeiro and Maibaum, 1992). The diagram structure suggests aspect introduction via an appropriate variant of graph transformation. Singlepushout rewriting in categories of total homomorphisms has already been used previously for different kinds of “enrichment” transformations; we identify “zigzag-path homomorphisms” as producing a category where many practically useful aspect introductions turn out to be such single-pushout transformations, and present the relevant theorems concerning pushout existence and pushout construction. Practical aspect introduction (e.g., privacy) always breaks some properties (e.g., “message can be read in transit”); therefore, aspect introduction transformations cannot be designed to be semantics preserving. Our special categorical setting enables selective reasoning about property preservation in the transformed specifications, and property introduction from the introduced aspects. This method enables us to detect and resolve both conflicts and undesirable emergent behaviors that arise from aspect introduction or interaction. We have developed tool support to introduce and analyze aspects at the system architecture level through zigzag graph transformation. The implementation is based on Hets, an initiative of Mossakowski et al. (2007) and consists of two key parts: the language development and the zigzag transformation. The development of the MFLogic language is based on the specification language Casl (Astesiano et al., 2002) and uses the logic introduced by Fiadeiro and Maibaum (1992). Besides parsing, syntactic and static semantics correctness checking, the language inclusion in Hets opens the door for automatic property preservation analysis and conflict detection. The main contribution of the tool support in Hets is the automatic aspect introduction and the “result architecture” generation by applying our zigzag graph transformation. / Thesis / Doctor of Philosophy (PhD)

For the modelling of chemistry we use undirected, labelled graphs as explicit models of molecules and graph transformation rules for modelling generalised chemical reactions. This is used to define artificial chemistries on the level of individual bonds and atoms, where formal graph grammars implicitly represent large spaces of chemical compounds. We use a graph rewriting formalism, rooted in category theory, called the Double Pushout approach, which directly expresses the transition state of chemical reactions. Using concurrency theory for transformation rules, we define algorithms for the composition of rewrite rules in a chemically intuitive manner that enable automatic abstraction of the level of detail in chemical pathways. Based on this rule composition we define an algorithmic framework for generation of vast reaction networks for specific spaces of a given chemistry, while still maintaining the level of detail of the model down to the atomic level. The framework also allows for computation with graphs and graph grammars, which is utilised to model non-trivial chemical systems. The graph generation relies on graph isomorphism testing, and we review the general individualisation-refinement paradigm used in the state-of-the-art algorithms for graph canonicalisation, isomorphism testing, and automorphism discovery. We present a model for chemical pathways based on a generalisation of network flows from ordinary directed graphs to directed hypergraphs. The model allows for reasoning about the flow of individual molecules in general pathways, and the introduction of chemically motivated routing constraints. It further provides the foundation for defining specialised pathway motifs, which is illustrated by defining necessary topological constraints for both catalytic and autocatalytic pathways. We also prove that central types of pathway questions are NP-complete, even for restricted classes of reaction networks. The complete pathway model, including constraints for catalytic and autocatalytic pathways, is implemented using integer linear programming. This implementation is used in a tree search method to enumerate both optimal and near-optimal pathway solutions. The formal methods are applied to multiple chemical systems: the enzyme catalysed beta-lactamase reaction, variations of the glycolysis pathway, and the formose process. In each of these systems we use rule composition to abstract pathways and calculate traces for isotope labelled carbon atoms. The pathway model is used to automatically enumerate alternative non-oxidative glycolysis pathways, and enumerate thousands of candidates for autocatalytic pathways in the formose process.

<p>The complex behavior of computer systems offers many challenges for <i>formal verification</i>. The analysis quickly becomes difficult as the number of participating processes increases.</p><p>A <i>parameterized system</i> is a family of systems parameterized on a number <i>n</i>, typically representing the number of participating processes. The <i>uniform verification problem</i> — to check whether a property holds for each instance — is an infinite-state problem. The automated analysis of parameterized and infinite-state systems has been the subject of research over the last 15–20 years. Much of the work has focused on safety properties. Progress in verification of liveness properties has been slow, as it is more difficult in general.</p><p>In this thesis, we consider verification of parameterized and infinite-state systems, with an emphasis on liveness, in the verification framework called <i>regular model checking (RMC)</i>. In RMC, states are represented as words, sets of states as regular expressions, and the transition relation as a regular relation.</p><p>We extend the automata-theoretic approach to RMC. We define a <i>specification logic</i> sufficiently strong to specify systems representable using RMC, and linear temporal logic properties of such systems, and provide an automatic translation from a specification into an analyzable model.</p><p>We develop <i>acceleration techniques</i> for RMC which allow more uniform and automatic verification than before, with greater power. Using these techniques, we succeed to verify safety and liveness properties of parameterized protocols from the literature.</p><p>We present a novel <i>reachability based</i> verification method for verification of liveness, in a general setting. We implement the method for RMC, with promising results.</p><p>Finally, we develop a framework for the verification of dynamic networks based on graph transformation, which generalizes the systems representable in RMC. In this framework we verify the latest version of the DYMO routing protocol, currently being considered for standardization by the IETF.</p>

Em contraste aos sistemas transformacionais, sistemas reativos são caracterisados por reagir continuamente a estímulos provinientes seu ambiente. Além da reatividade, se considerarmos que muitas aplicações requerem métodos de especificação que possibilitam descrever a distribuição espacial dos estados, sistemas de transformação de grafos parecem ser uma técnica de especificação bastante adequada. Algumas aplicações com essas características são sistemas móveis e vias biológicas. Além disso, diversas abordagens para especificação de sistemas reativos propõem usar linguagens assíncronas para especificar a comunicação entre componentes e definem mecanismos para descrever um conjunto (ou seqüência) de atividades que são realizadas atomicamente. Porém, pouca atenção tem sido dada à idéia de estender sistemas de transformação de grafos para permitir a especificação de atividades atômicas. Recentemente, inspirada nas idéias das redes de Petri “zero-safe” foi definida uma extensão de sistemas de transformação de grafos (GTS) – denominada GTS transacional (T-GTS) – equipando-os com uma noção de transação. Uma transação, nesta abordagem, descreve um conjunto de ações que são executadas de um modo atômico e é definida através de uma distinção entre os recursos visíveis e invisíveis de um ponto de vista externo, onde os últimos são considerados temporários e “esquecidos” em um nível abstrato. Nesta tese é dada uma fundamentação mais teórica para T-GTSs definindo uma noção de morfismos de implementação T-GTS (associando produções de um sistema com transações de outro) e, usando essa noção, é demonstrada a existência de uma adjunção entre as categorias de GTSs e T-GTSs com morfismos de implementação. Além disso, GTSs transacionais são estendidas com um mecanismo para descrever padrões de interação de sistemas reativos através de relações de dependência incluídas nas produções. A idéia é que um sitema interage com seu ambiente consumindo e criando elementos visíveis para à esse ambiente, uma relação de causalidade. Finalmente, propomos uma noção de refinamento para T-GTSs com relação de dependência caracterizada por uma visão “caixa-devidro”, onde alguns aspectos internos são preservados. Em um nível abstrato, o sistema é especificado por produções que descrevem (de uma maneira atômica) reações completas, onde a relação de dependência determina algumas restrições na estrutura interna dessas reações. Um refinamento de um sistema é definido por um morfismo total de implementação que associa cada produção (abstrata) a uma transação. Assim, o sistema refinado preserva todo o comportamento externo do sistema original e as restrições da estrutura interna determinadas pelas relações de dependência. / Reactive systems, in contrast to transformational systems, are characterised by having to continuously react to stimuli from its environment. If, in addition to reactiveness, we consider that for many applications the specification method should provide a way to describe the spatial distribution of states, graph transformation seems to be a suitable specification technique. Some applications with these characteristics are mobile systems and biological pathways. However, the approaches provided for graph transformations so far are not adequate to explicitly describe interaction patterns. Furthermore, several approaches to specify reactive systems propose to use asynchronous languages to specify communication between components and define mechanisms to describe a set (or sequence) of activities that are performed atomically. However, scarce attention has been devoted to the idea of extending GTSs in order to allow the specification of atomic activities. Inspired by the ideas of zero-safe Petri nets, an extension of graph transformation systems (GTSs) – called transactional GTS (T-GTS) – was defined, equipping them with a transaction notion. A transaction, in this approach, describes a set of actions that are executed in an atomic way and it is defined by distinguishing the resources that are visible or invisible from an external point of view, where the last ones are considered temporary and are forgotten at a more abstract level. In this thesis, we give a more theoretical foundation to T-GTS defining a notion of implementation morphisms between T-GTSs (associating graph productions of a system with transactions of other system) and using this notion we demonstrate the existence of an adjunction between categories of GTSs and T-GTSs with implementation morphisms. Moreover, we extends transactional GTSs with a mechanism to describe interaction patterns of reactive systems, by means of dependency relations included in the graph productions. The idea is that a system interacts with its environment by consuming and creating elements visible to this environment, obeying a causal dependency. Finally, we propose a notion of glass-box refinement for T-GTSs with dependency relations, where some internal aspects are preserved. In an abstract level, the system is specified by productions describing (in an atomic way) complete reactions, where the dependency relations give some constraints on the internal structure of these reactions. A refinement of a system is given by a total implementation morphism, that associates each (abstract) production to a transaction. Hence, the refined system preserves all external behaviour of the original system and the internal constraints given by the dependency relations.

The Unified Modelling Language (UML) is intended to express complex ideas in an intuitive and easily understood way. It is important because it is widely used in software engineering and other disciplines. Although an official definition document exists, there is much debate over the precise meaning of UML models. ¶ In response, the academic community have put forward many different proposals for formalising UML, but it is not at all obvious how to decide between them. Indeed, given that UML practitioners are inclined to reject formalisms as non-intuitive, it is not even obvious that the definition should be “formal” at all. Rather than searching for yet another formalisation of UML, our main aim is to determine what would constitute a good definition of UML. ¶ The first chapter sets the UML definition problem in a broad context, relating it to work in logic and the philosophy of science. More specific conclusions about the nature of model driven development are reached in the beginning of Chapter 2. We then develop criteria for a definition of UML. Applying these criteria to the existing definition, we find that it is lacking in clarity. We then set out to test the precision of the definition. The test is to take an apparently inconsistent model, and determine whether it really is inconsistent according to the definition. ¶ Many people have proposed that UML models are graphs, but few have justified this choice using the official definition of UML. We begin Chapter 3 by arguing from the official definition that UML models are graphs and that instantiation is a graph homomorphism into an interpretation functor. The official definition of UML defines the semantics against its abstract syntax, which is in turn defined by a UML model. Chapters 3 and 4 prepare for our test by resolving this apparent circularity. The result is a semantics for the metamodel fragment of the language. ¶ In Chapter 5, we find, contrary to popular belief, that the official definition does provide sufficient semantics to classify the example model as inconsistent. Moreover, the sustained study of the semantics in Chapters 3 to 5 confirms our initial argument that the semantic domain is graphs. The Actions are the building blocks of UML’s prescriptive dynamics. We see that they can be naturally defined as graph transformation rules. Sequence diagrams are the main example of descriptive dynamics, but we find that their official semantics are broken. The “recorded history” approach should be replaced, we suggest, by a graph-oriented dynamic logic. ¶ Chapter 6 presents our early work on dynamic logic for UML sequence diagrams and further explores the proposed semantic repairs. In Chapter 7, guided by the criteria developed in Chapter 2, we critically survey the UML formalisation literature and conclude that an existing body of graph transformation based work known as “dynamic metamodelling” is very close to what is required. ¶ The final chapter draws together our conclusions. It proposes a category theoretic construction to merge models of the syntax and semantic domain, yielding a type graph for the graph transformation system which defines the dynamic semantics of the language. Finally, it outlines the further work required to realise a satisfactory definition of UML.

The complex behavior of computer systems offers many challenges for formal verification. The analysis quickly becomes difficult as the number of participating processes increases. A parameterized system is a family of systems parameterized on a number n, typically representing the number of participating processes. The uniform verification problem — to check whether a property holds for each instance — is an infinite-state problem. The automated analysis of parameterized and infinite-state systems has been the subject of research over the last 15–20 years. Much of the work has focused on safety properties. Progress in verification of liveness properties has been slow, as it is more difficult in general. In this thesis, we consider verification of parameterized and infinite-state systems, with an emphasis on liveness, in the verification framework called regular model checking (RMC). In RMC, states are represented as words, sets of states as regular expressions, and the transition relation as a regular relation. We extend the automata-theoretic approach to RMC. We define a specification logic sufficiently strong to specify systems representable using RMC, and linear temporal logic properties of such systems, and provide an automatic translation from a specification into an analyzable model. We develop acceleration techniques for RMC which allow more uniform and automatic verification than before, with greater power. Using these techniques, we succeed to verify safety and liveness properties of parameterized protocols from the literature. We present a novel reachability based verification method for verification of liveness, in a general setting. We implement the method for RMC, with promising results. Finally, we develop a framework for the verification of dynamic networks based on graph transformation, which generalizes the systems representable in RMC. In this framework we verify the latest version of the DYMO routing protocol, currently being considered for standardization by the IETF.

Em contraste aos sistemas transformacionais, sistemas reativos são caracterisados por reagir continuamente a estímulos provinientes seu ambiente. Além da reatividade, se considerarmos que muitas aplicações requerem métodos de especificação que possibilitam descrever a distribuição espacial dos estados, sistemas de transformação de grafos parecem ser uma técnica de especificação bastante adequada. Algumas aplicações com essas características são sistemas móveis e vias biológicas. Além disso, diversas abordagens para especificação de sistemas reativos propõem usar linguagens assíncronas para especificar a comunicação entre componentes e definem mecanismos para descrever um conjunto (ou seqüência) de atividades que são realizadas atomicamente. Porém, pouca atenção tem sido dada à idéia de estender sistemas de transformação de grafos para permitir a especificação de atividades atômicas. Recentemente, inspirada nas idéias das redes de Petri “zero-safe” foi definida uma extensão de sistemas de transformação de grafos (GTS) – denominada GTS transacional (T-GTS) – equipando-os com uma noção de transação. Uma transação, nesta abordagem, descreve um conjunto de ações que são executadas de um modo atômico e é definida através de uma distinção entre os recursos visíveis e invisíveis de um ponto de vista externo, onde os últimos são considerados temporários e “esquecidos” em um nível abstrato. Nesta tese é dada uma fundamentação mais teórica para T-GTSs definindo uma noção de morfismos de implementação T-GTS (associando produções de um sistema com transações de outro) e, usando essa noção, é demonstrada a existência de uma adjunção entre as categorias de GTSs e T-GTSs com morfismos de implementação. Além disso, GTSs transacionais são estendidas com um mecanismo para descrever padrões de interação de sistemas reativos através de relações de dependência incluídas nas produções. A idéia é que um sitema interage com seu ambiente consumindo e criando elementos visíveis para à esse ambiente, uma relação de causalidade. Finalmente, propomos uma noção de refinamento para T-GTSs com relação de dependência caracterizada por uma visão “caixa-devidro”, onde alguns aspectos internos são preservados. Em um nível abstrato, o sistema é especificado por produções que descrevem (de uma maneira atômica) reações completas, onde a relação de dependência determina algumas restrições na estrutura interna dessas reações. Um refinamento de um sistema é definido por um morfismo total de implementação que associa cada produção (abstrata) a uma transação. Assim, o sistema refinado preserva todo o comportamento externo do sistema original e as restrições da estrutura interna determinadas pelas relações de dependência. / Reactive systems, in contrast to transformational systems, are characterised by having to continuously react to stimuli from its environment. If, in addition to reactiveness, we consider that for many applications the specification method should provide a way to describe the spatial distribution of states, graph transformation seems to be a suitable specification technique. Some applications with these characteristics are mobile systems and biological pathways. However, the approaches provided for graph transformations so far are not adequate to explicitly describe interaction patterns. Furthermore, several approaches to specify reactive systems propose to use asynchronous languages to specify communication between components and define mechanisms to describe a set (or sequence) of activities that are performed atomically. However, scarce attention has been devoted to the idea of extending GTSs in order to allow the specification of atomic activities. Inspired by the ideas of zero-safe Petri nets, an extension of graph transformation systems (GTSs) – called transactional GTS (T-GTS) – was defined, equipping them with a transaction notion. A transaction, in this approach, describes a set of actions that are executed in an atomic way and it is defined by distinguishing the resources that are visible or invisible from an external point of view, where the last ones are considered temporary and are forgotten at a more abstract level. In this thesis, we give a more theoretical foundation to T-GTS defining a notion of implementation morphisms between T-GTSs (associating graph productions of a system with transactions of other system) and using this notion we demonstrate the existence of an adjunction between categories of GTSs and T-GTSs with implementation morphisms. Moreover, we extends transactional GTSs with a mechanism to describe interaction patterns of reactive systems, by means of dependency relations included in the graph productions. The idea is that a system interacts with its environment by consuming and creating elements visible to this environment, obeying a causal dependency. Finally, we propose a notion of glass-box refinement for T-GTSs with dependency relations, where some internal aspects are preserved. In an abstract level, the system is specified by productions describing (in an atomic way) complete reactions, where the dependency relations give some constraints on the internal structure of these reactions. A refinement of a system is given by a total implementation morphism, that associates each (abstract) production to a transaction. Hence, the refined system preserves all external behaviour of the original system and the internal constraints given by the dependency relations.