Search

Model management is a central activity in Software Engineering. The most challenging aspect of model management is to keep inter-related models consistent with each other while they evolve. As a consequence, there is a lot of scientific activity in this area, which has produced an extensive body of knowledge, methods, results and tools. The majority of these approaches, however, are limited to binary inter-model relations; i.e. the synchronisation of exactly two models. Yet, not every multi-ary relation can be factored into a family of binary relations. In this paper, we propose and investigate a novel comprehensive system construction, which is able to represent multi-ary relations among multiple models in an integrated manner and thus serves as a formal foundation for artefacts used in consistency management activities involving multiple models. The construction is based on the definition of partial commonalities among a set of models using the same language, which is used to denote the (local) models. The main theoretical results of this paper are proofs of the facts that comprehensive systems are an admissible environment for (i) applying formal means of consistency verification (diagrammatic predicate framework), (ii) performing algebraic graph transformation (weak adhesive HLR category), and (iii) that they generalise the underlying setting of graph diagrams and triple graph grammars.

Mapping nodes in multi-layer and heterogeneous networks to low-dimensional vectors has wide applications in community detection, node classification and link prediction, etc. In this paper, a generalized graph representation learning framework is proposed for information aggregation in various multi-layer and heterogeneous networks. Specifically, an aggregation network is firstly obtained by graph transformation, generating potential information links based on the network structure on different layers. A comprehensive measurement of the similarity between different nodes in the aggregation network is then carried out by aggregating the information of nodes’ identities of structure, nearness and attributes etc. Based on the comprehensive similarity values the nodes have, a context graph can be generated using a simple edge percolation method, which provides a basis facilitating some important downstream work such as classification, clustering and prediction etc. We demonstrate the effectiveness of the new framework in identifying subnetworks in a cyberspace network, where it significantly outperforms all the existing baselines. Ministry of Education (MOE) G.Y. and Y.K. were supported by NSSFC 2019-SKJJ-C-005. G.X. was supported by the Ministry of Education (MOE), Singapore, under contract RG19/20.

The ability to assess the reliability of safety-critical systems is one of the most crucial requirements in the design of modern safety-critical systems where even a minor failure can result in loss of life or irreparable damage to the environment. Model checking is an automatic technique that verifies or refutes system properties by exploring all reachable states (state space) of a model. In large and complex systems, it is probable that the state space explosion problem occurs. In exploring the state space of systems modeled by graph transformations, the rule applied on the current state specifies the rule that can perform on the next state. In other words, the allowed rule on the current state depends only on the applied rule on the previous state, not the ones on earlier states. This fact motivates us to use a Markov chain (MC) to capture this type of dependencies and applies the Estimation of Distribution Algorithm (EDA) to improve the quality of the MC. EDA is an evolutionary algorithm directing the search for the optimal solution by learning and sampling probabilistic models through the best individuals of a population at each generation. To show the effectiveness of the proposed approach, we implement it in GROOVE, an open source toolset for designing and model checking graph transformation systems. Experimental results confirm that the proposed approach has a high speed and accuracy in comparison with the existing meta-heuristic and evolutionary techniques in safety analysis of systems specified formally through graph transformations.

Electrocardiography (ECG) signal recognition is one of the popular research topics for machine learning. In this paper, a novel transformation called tower graph transformation is proposed to classify ECG signals with high accuracy rates. It employs a tower graph, which uses minimum, maximum and average pooling methods altogether to generate novel signals for the feature extraction. In order to extract meaningful features, we presented a novel one-dimensional hexadecimal pattern. To select distinctive and informative features, an iterative ReliefF and Neighborhood Component Analysis (NCA) based feature selection is utilized. By using these methods, a novel ECG signal classification approach is presented. In the preprocessing phase, tower graph-based pooling transformation is applied to each signal. The proposed one-dimensional hexadecimal adaptive pattern extracts 1536 features from each node of the tower graph. The extracted features are fused and 15,360 features are obtained and the most discriminative 142 features are selected by the ReliefF and iterative NCA (RFINCA) feature selection approach. These selected features are used as an input to the artificial neural network and deep neural network and 95.70% and 97.10% classification accuracy was obtained respectively. These results demonstrated the success of the proposed tower graph-based method.

Safety is one of the most important features of modern software systems, especially safety-critical systems such as nuclear power plants, which can be checked exactly by model checking. Model checking is a formal verification technique that analyzes system properties through exploring all reachable states (state space) of a model of a system. The problem of the technique is that it confronts the state space explosion in large and complex systems due to exponential memory usage. Recent researches show that a partial and intelligent exploration of the state space can be a suitable solution to overcome this problem. In this paper, we propose a two-phase model checking for safety analysis of systems specified formally through graph transformations. In the first phase, the beam-search algorithm explores the state space to a specific number of states. In case of failure of the phase, the second phase starts: in systems specified through graph transformations, the rule applied on the previous state can determine the rule that can perform on the next state. In other words, the rule on current state depends on only the rule applied to previous state, not the one on earlier states. Hence, a Markov chain (MC) is estimated to capture dependencies between the sequence of applied rules in the state space explored by the beam-search algorithm. The MC is then employed to explore the remainder of the state space intelligently. To evaluate the effectiveness of the two-phase model checking, we implement it in GROOVE, an open source toolset for designing and model checking graph transformation systems. Experimental results show that the two-phase model checking has the high speed and accuracy in comparison with the existing meta-heuristic and evolutionary techniques.

The basic principle of graph rewriting is the stepwise replacement of subgraphs inside a host graph. A challenge in such replacement steps is the treatment of the patch graph, consisting of those edges of the host graph that touch the subgraph, but are not part of it. We introduce patch graph rewriting, a visual graph rewriting language with precise formal semantics. The language has rich expressive power in two ways. First, rewrite rules can flexibly constrain the permitted shapes of patches touching matching subgraphs. Second, rules can freely transform patches. We highlight the framework’s distinguishing features by comparing it against existing approaches.

In this paper we describe our system for automatically extracting "correct" programs from proofs using a development for the Curry-Howard process. Although program extraction has been developed by many authors (see [5,?,?]), our system has a number of novel features designed to make it very easy to use and as close as possible to ordinary mathematical terminology and practice. These features include 1. the use of Henkin's technique [6] to reduce higher-order logic to many-sorted (first-order) logic 2. the free use of new rules for induction subject to certain conditions 3. the extensive use of previously programmed (primitive) recursive functions. 4. the use of templates to make the reasoning much closer to normal mathematical proffs. 5. an extension of the technique of the use of Harrop formulae to classically true formulae (cf. the footnote on p.101 in Kreisel [9]); As an example of our system we give a constructive proof of the well-known theorem that every graph of even parity, which is non-trivial in the sense that it does not consist of isolated vertices, has a cycle. Given such a graph as input, the extracted program produces a cycle as promised.

Constrained graph layout is a recent generalisation of force-directed graph layout which allows constraints on node placement. We give a constrained graph layout algorithm that takes an initial feasible layout and improves it while preserving the topology of the initial layout. The algorithm supports poly-line connectors and clusters. During layout the connectors and cluster boundaries act like impervious rubber-bands which try to shrink in length. The intended application for our algorithm is dynamic graph layout, but it can also be used to improve layouts generated by other graph layout techniques.

Designing and reasoning about complex systems such as wireless sensor networks is hard due to highly dynamic environments: sensors are heterogeneous, battery-powered, and mobile. While formal modelling can provide rigorous mechanisms for design/reasoning, they are often viewed as difficult to use. Graph rewrite-based modelling techniques increase usability by providing an intuitive, flexible, and diagrammatic form of modelling in which graph-like structures express relationships between entities while rewriting mechanisms allow model evolution. Two major graph-based formalisms are Graph Transformation Systems (GTS) and Bigraphical Reactive Systems (BRS). While both use similar underlying structures, how they are employed in modelling is quite different. To gain a deeper understanding of GTS and BRS, and to guide future modelling, theory, and tool development, in this experience report we compare the practical modelling abilities and style of GTS and BRS when applied to topology control in WSNs. To show the value of the models, we describe how analysis may be performed in both formalisms. A comparison of the approaches shows that although the two formalisms are different, from both a theoretical and practical modelling standpoint, they are each successful in modelling topology control in WSNs. We found that GTS, while featuring a small set of entities and transformation rules, relied on entity attributes, rule application based on attribute/variable side-conditions, and imperative control flow units. BRS on the other hand, required a larger number of entities in order to both encode attributes directly in the model (via nesting) and provide tagging functionality that, when coupled with rule priorities, implements control flow. There remains promising research mapping techniques between the formalisms to further enable flexible and expressive modelling.

With the constant research and development of Transactional Memory (TM) systems, various algorithms have been proposed, and their correctness is always an important aspect to take into account. When analyzing TM algorithms, one of the most commonly used correctness criterion is opacity, which infers that the algorithm only generates executions that observe consistent states of the shared memory. In this work we present a formal definition to demonstrate that a given TM algorithm only generates opaque histories using a Graph Transformation System (GTS). We achieve that by introducing a methodology of translating an algorithm into production rules that manipulate the state of a graph. With a set initial state of transactions, the result of this method consists of a state space that includes every possible order of execution of transactional operations that are automatically checked for opacity, therefore all possible histories the algorithm can generate are checked for the safety property. As a case study we demonstrate our approach using the algorithm CaPR+.

We employ a triple graph grammar to enable configurable conversion from IFC to CityGML. In this paper, we present the mathematical framework behind the graph transformation approach as well as an application to create, store and maintain transformation rules implementing this framework. Particular emphasis is put on how the approach enables graphical representation and static analysis of rules and rulesets, both in the theoretical framework and prototypical implementation. Even if various publications and tools for general graph transformation do already exist, we hope that the BIM–GIS community will benefit from a domain-specific introduction to the theory and dedicated software tools.

Context Test generation by model checking is a useful technique in model-based testing that allows automatic generation of test cases from models by utilizing the counter-examples/witnesses produced through a model checker. However, generating redundant test cases and state space explosion problem are two major obstacles to transfer this technique into industrial practice. Objective An idea to cope with these challenges consists in an intelligent model checking for exploring only a portion of the state space according to the test objectives. Motivated by this idea, we propose an approach that exploits meta-heuristic algorithms to adapt a model checker when used for integration testing of systems formally specified by graph transformations. Method This method is not based on model checking algorithms, but rather uses the modeling and simulation features of the underlying model checker. In the proposed approach, a population of test suites that each of which is a set of paths on the state space, is evolved towards satisfying the all def-use test objectives. Consequently, a test suite with high coverage is generated. Results To assess the efficiency of our approach, it is implemented in GROOVE, an open source toolset for designing and model checking graph transformation systems. Empirical results based on some case studies, confirm a significant improvement in terms of coverage, speed and memory usage, in comparison with the state of the art techniques. Conclusion Our analysis reveals that intelligent model checking can appropriately address the challenges of traditional model-checking-assisted testing. We further conclude that graph transformation specification is an efficient modeling solution to behavioral testing and graph transformation tools have a great potential for developing a model-based testing tool.

Program logics typically reason about an over-approximation of program behaviour to prove the absence of bugs. Recently, program logics have been proposed that instead prove the presence of bugs by means of under-approximate reasoning, which has the promise of better scalability. In this paper, we present an under-approximate program logic for a nondeterministic graph programming language, and show how it can be used to reason deductively about program incorrectness, whether defined by the presence of forbidden graph structure or by finitely failing executions. We prove this ‘incorrectness logic’ to be sound and complete, and speculate on some possible future applications of it.

In this work, we introduce KnitKit , a flexible and customizable system for the computational design and production of functional, multi-material, and three-dimensional knitted textiles. Our system greatly simplifies the knitting of 3D objects with complex, varying patterns that use multiple yarns and stitch patterns by separating the high-level design specification in terms of geometry, stitch patterns, materials or colors from the low-level, machine-specific knitting instruction generation. Starting from a triangular 3D mesh and a 2D texture that specifies knitting patterns on top of the geometry, our system generates the required machine instructions in three major steps. First, the input is processed and the KnitNet data structure is generated. This graph structure serves as an abstract interface between the high-level geometric and knitting configuration and the low-level, machine-specific knitting instructions. Second, a graph rewriting procedure is applied on the KnitNet that produces a sequence of abstract machine actions. Finally, the low-level machine instructions are generated by adapting those abstract actions to a specific machine context. We showcase the potential of this computational approach by designing and fabricating a variety of objects with complex geometries, multiple yarns, and multiple stitch patterns.

Software, whether desktop, mobile or web, is becoming more and more connected. Software development is also becoming more connected with ecosystems comprised of networks of millions of packages. Engineering software today is writing code that weaves together libraries, services and applications. Such fabrics are under constant changes due to both internal requests, e.g. new features, or external demands, e.g. dependency updates. Avoiding integration bugs in this scenario can be a big challenge regardless of common strategies such as testing and versioning. We propose an approach, called Module Integration using Graph Grammars (MIGRATE), to describe/analyze integration points among software modules. We define module nets, a formalism to capture the essential information regarding module integration, whose semantics is defined in terms of graph transformations. This allows us to use the rich theory of graph transformation, specially critical pair analysis, to analyze the coupling among different modules and create warnings in case of possible integration problems. The approach is organized in three phases: (i) transformation of code into module nets (model extraction), (ii) translation of module nets into graph grammars (semantics of integration) and (iii) verification of module integration. We have built a prototype that implements the MIGRATE approach.

To verify graph programs in the language GP 2, we present a monadic second-order logic with counting and a Hoare-style proof calculus. The logic has quantifiers for GP 2’s attributes and for sets of nodes or edges. This allows to specify non-local graph properties such as connectedness, k-colourability, etc. We show how to construct a strongest liberal postcondition for a given graph transformation rule and a precondition. The proof rules establish the total correctness of graph programs and are shown to be sound. They allow to verify more programs than is possible with previous approaches. In particular, many programs with nested loops are covered by the calculus.

The paper presents a new application of the graph model of the game world and graph rules describing players’ actions in this world. This time, this model and rules are used to design storylines in multiplayer role-playing games. The proposed model is suitable for collaborative plot design, as the set of rules describing game actions can be divided into subsets corresponding to particular quests, which are then assigned to different plot writers. The main contributions of this paper are: firstly, a new type of graph transformation rules for construction of storylines in games that require competition or collaboration between multiple players, and secondly, a prototype networked application to validate the proposed ideas and to serve as a playtesting tool for the designed sets of rules. In the presented application, the graph world model is stored in a Neo4j graph database server. Application instances running on players’ computers communicate with this server. The paper presents the application’s operation on an example of a simple two-player game.

We present a tool that checks for a given context-free graph grammar whether the corresponding graph reduction system in which all rules are applied backward, is confluent—a question that arises when using graph grammars to guide state space abstractions for analyzing heap-manipulating programs; confluence of the graph reduction system then guarantees the abstraction’s uniqueness. If a graph reduction system is not confluent, our tool provides symbolic representations of counterexamples to confluence, i.e., non-joinable critical pairs, for manual inspection. Furthermore, it features a heuristics-based completion procedure that attempts to turn a graph reduction system into a confluent one without invalidating the properties mandated by the abstraction framework. We evaluate our implementation on various graph grammars for verifying data structure traversal algorithms from the literature.

International audience; This paper introduces SetUp, a theoretical and applied framework for the management of RDF/S database evolution on the basis of graph rewriting rules. Rewriting rules formalize instance or schema changes, ensuring graph’s consistency with respect to given constraints. Constraints considered in this paper are a well known variant of RDF/S semantic, but the approach can be adapted to user-defined constraints. Furthermore, SetUp manages updates by ensuring rule applicability through the generation of side-effects: new updates which guarantee that rule application conditions hold.We provide herein formal validation and experimental evaluation of SetUp.

model checking techniques are often used for the verification of software systems. Such techniques are accompanied with several advantages. However, state space explosion is one of the drawbacks to model checking. During recent years, several methods have been proposed based on evolutionary and meta-heuristic algorithms to solve this problem. In this paper, a hybrid approach is presented to cope with the SSE problem in model checking of systems modeled by GTS with an ample state space. Most of existence proposed methods that aim to verify systems are applied to detect deadlocks by graph transformations. The proposed approach is based on the fuzzy genetic algorithm and is designed to decline the safety property by verifying the reachability property and detecting deadlocks. In this solution, the state space of the system is searched by a fuzzy genetic algorithm to find the state in which the specified property is refuted/verified. To implement and evaluate the suggested approach, GROOVE is used as a powerful designing and model checking toolset in GTS. The experimental results indicate that the presented hybrid fuzzy method improves speed and performance by comparing other techniques

We present new algorithms to compute candidate keys and third normal form design of a relational database schema, using strategic port graph rewriting. More precisely, we define port graph rewriting rules and strategies that implement a candidate key definition and Ullman’s algorithm to decompose a relation schema into lossless 3NF schemata. We show the correctness of the resulting database schema by proving soundness, completeness and termination of our strategic graph programs. These rules and strategies provide a declarative and visual description of the algorithms, and permit a fine-grained analysis of the computation steps involved in the normalisation process. The algorithms have been implemented in Porgy, a visual, interactive modelling tool.

The double pushout approach for graph transformation naturally allows an abstraction level of biochemical systems in which individual atoms of molecules can be traced automatically within chemical reaction networks. Aiming at a mathematical rigorous approach for isotope labeling design, we convert chemical reaction networks (represented as directed hypergraphs) into transformation semigroups. Symmetries within molecules correspond to permutations, whereas (not necessarily invertible) chemical reactions define the transformations of the semigroup. An approach for the automatic inference of informative labeling of atoms is presented, which allows to distinguish the activity of different pathway alternatives within reaction networks. To illustrate our approaches, we apply them to the reaction network of glycolysis, which is an important and well-understood process that allows for different alternatives to convert glucose into pyruvate.

In Domain-Specific Modelling (DSM) the general goal is to provide Domain-Specific Modelling Languages (DSMLs) for domain users to model systems using concepts and notations they are familiar with, in their problem domain. Verifying whether a model satisfies a set of requirements is considered to be an important challenge in DSM, but is nevertheless mostly neglected. We present a solution in the form of ProMoBox, a framework that integrates the definition and verification of temporal properties in discrete-time behavioural DSMLs, whose semantics can be described as a schedule of graph rewrite rules. Thanks to the expressiveness of graph rewriting, this covers a very large class of problems. With ProMoBox, the domain user models not only the system with a DSML, but also its properties, input model, run-time state and output trace. A DSML is thus comprised of five sublanguages, which share domain-specific syntax, and are generated from a single metamodel. Generic transformations to and from a verification backbone ensure that both the language engineer and the domain user are shielded from underlying notations and techniques. We explicitly model the ProMoBox framework's process in the paper. Furthermore, we evaluate ProMoBox to assert that it supports the specification and verification of properties in a highly flexible and automated way.

The elegance of the single-pushout (SPO) approach to graph transformations arises from substituting total morphisms by partial ones in the underlying category. Thus, SPO’s applicability depends on the durability of pushouts after this transition. There is a wide range of work on the question when pushouts exist in categories with partial morphisms starting with the pioneering work of Lowe and Kennaway and ending with an essential characterisation in terms of an exactness property (for the interplay between pullbacks and pushouts) and an adjointness condition (w.r.t. inverse image functions) by Hayman and Heindel.

We have defined a graph transformation step as the application of a rule, defined over a type graph and a rule signature, to a given instance graph and producing a derived graph in a single, atomic action. In software modelling, individual actions are often combined into processes describing, for example, a business transaction or the implementation of a complex operation. The problem of controlling the application of rules, for example to ensure that certain actions happen in the right order, is the subject of this section.

International audience; We propose to use strategic port graph rewriting as a visual modelling tool to analyse financial market processes. We illustrate the approach by specifying a basic "rational negligence" model in which investors may choose to trade securities without performing independent evaluations of the underlying assets. We show that our model is correct with respect to the equational model and can be used to simulate simple market behaviours. The model has been implemented within PORGY, a graph-based specification and simulation environment.

State-of-the-art approaches to controlled graph rewriting focus on the specification of an external control layer over graph-rewriting rule applications and on the input-output semantics of the resulting systems, leading to a decreased relevance of many interesting operational aspects of graph transformation, as studied in the classical theory of algebraic graph rewriting. We propose a novel approach to controlled graph rewriting where we aim at bridging the gap between these two complementary approaches, defining an operational semantics for which classical concepts and results related to independence and parallelism of graph derivations can be recast. The calculus we propose is based on a control layer specified using (a fragment of) Milner's Calculus of Communicating Systems (CCS), where the actions specify the application of graph transformation rules to the current state, according to the Double-Pushout approach (DPO). In particular, we address the following aspects for our controlled graph-rewriting processes: (i) expressiveness of the control language, compared to a minimally complete reference language, Graph Programs, proposed by Habel and Plump; (ii) process equivalence based on labeled transition systems and a structural operational semantics; (iii) a unifying treatment of action independence, considering the corresponding notions from both process algebra and graph-rewriting theory; and (iv) parallelism and concurrency based on the notion of asynchronous (labeled) transition systems, obtained from an asynchronous version of the proposed calculus.

This paper is concerned with representing graphs and graph transformation rules using ASCII text only. It proposes an approach based on the textual graph representation used in Cypher Query Language and PGQL. Replacing visual rule languages with a pure text-based language eliminates the need for specialized graphical rule editors. Instead, standard software engineering tools can be used to collaboratively develop a set of graph rules.

Attributed graph grammars can specify the transformation of complex data and object structures within a natural rule-based model of concurrency. This is crucial to their use in modelling interfaces of services and components as well as the evolution of complex systems and networks. However, the established concurrent semantics of graph grammars by unfolding does not cover attributed grammars. We develop a theory of unfolding for attributed graph grammars where attribution is represented symbolically, via logical constraints. We establish a functorial representation (a coreflection) of unfolding which guarantees it to be correct, complete and fully abstract.

Model checking is one of the successful techniques in automated verification of software and hardware systems. However, employing this technique for verification of properties such as the safety and liveness requires that all possible states of a system are generated and then the given property is checked. In large and complex systems, generating all states causes the state space explosion problem. Hence, it is possible to refute such properties by searching the state space to find a state in which the given property is violated. Of course, it is possible that detecting such states in complex systems leads to the exhaustive exploration of the state space. Recent researches confirm that using meta-heuristic and evolutionary approaches to intelligently explore a portion of the state space can be a promising idea. Hence, in this paper, we propose an approach based on ant colony optimization algorithm for refuting the safety and liveness properties and also analyzing reachability ones in systems specified formally through graph transformation system. Refutation of liveness and analyzing reachability properties in systems modeled by graph transformations are the prominent advantages of this approach in comparison with the previous approaches. The proposed approach is implemented in GROOVE which is an open source toolset for designing and model checking graph transformation systems. Experimental results show that our proposed approach is faster and it generates shorter counterexamples in comparison with others.

We present strategic port graph rewriting as a basis for the implementation of visual modelling tools. The goal is to facilitate the specification and programming tasks associated with the modelling of complex systems. A system is represented by an initial graph and a collection of graph rewrite rules, together with a user-defined strategy to control the application of rules. The traditional operators found in strategy languages for term rewriting have been adapted to deal with the more general setting of graph rewriting, and some new constructs have been included in the strategy language to deal with graph traversal and management of rewriting positions in the graph. We give a formal semantics for the language, and describe its implementation: the graph transformation and visualisation tool Porgy.

Various designs of CVTs were explored from two points of view: analysis of the design itself and analysis of the methods and techniques, used in the process of creation of the CVT. To solve the problem of finding new designs of mechanisms, the graph transformation method was developed. It includes the following heuristic techniques: a decrease in the number of graph nodes at simplification of a design or to remove non-essential elements; a change in location of graph edges and comparison of a new location of edges and necessary changes in a design; a search for all possible options for location of the parts that correspond to the same graph; introduction to the graph of the nodes, corresponding to the property, for implementation of which a part (a node) can be added to a design or, vice versa, can be removed from a design, and the property it implemented will be implemented by other parts. The original design of the CVT, in which load is transmitted by gear engagement without using friction disks and flexible sections, was developed. A continuously variable of transition ratio is ensured by a gear wheel with a variable pitch. The gear wheel consists of three gear sectors, two of which are involved in meshing. The third unloaded sector performs a turn with angular velocity that is higher than velocity of rotation of the output shaft until it takes a position before coming into engagement. The CVT does not have such drawback as fluctuations of transmission ratio. Based on the analysis of the bond-graphs, efficiency was determined, which depending on velocity of the output shaft is in the range of 95…97%. The disadvantage of the developed design is an insufficiently wide gear ratio range R=1.5…1.6, which is limited by transverse contact ratio ε&alpha

In modern system-on-chip (SoC) designs, IP-reuse is considered a driving force to increase productivity. To support various designs, a huge amount of Intellectual Property (IP) hardware blocks have been developed. The integration of those IPs into an SoC may require significant effort—up to days or weeks depending on experience and complexity. This article presents a novel approach to significantly reduce the design effort to bring-up a working SoC design by automatic IP integration as part of a library-based Software-defined SoC flow. In detail, the IP-supplier prepares a HW-accelerated software library (HASL) for the SoC architect, who wants to use the IP in an SoC design. As a key point of our approach, integration knowledge is encoded in the library as a set of integration rules. These rules are defined in the machine-readable standardized IP-XACT format by the IP supplier, who has a good knowledge of the IP’s hardware details. The library preparation step on the IP supplier’s side is also partly automated in the proposed flow, including a partial generation of configurable HW drivers, schedulers, and the software library functions. For the SoC architect, we have developed the graph-grammar-based IP-integration (GRIP) tool. The software application is developed using the functions supplied in the HASL. According to the calls to the HASL functions, the GRIP tool automatically integrates IP-blocks using the rule information supplied with the library and runs a full Design Space Exploration. For this, the SoC architecture and rules are transformed into the graph domain to apply graph rewriting methods. The GRIP tool is model-driven and based on the Eclipse Modeling Framework. With code generation techniques, SoC candidate architectures can be transformed to hardware descriptions for the target platform. The HW/SW interfaces between SW library functions and IP blocks can be automatically generated for bare-metal or Linux-based applications. The approach is demonstrated with two case-studies on the Xilinx Zynq-based ZedBoard evaluation board using a HASL for computer vision. It can yield 10×-150× performance improvement for the bare-metal application versions and 4×--7× performance improvement for the Linux-based application versions, when executed on an optimized HW-accelerated SoC architecture compared to a non HW-accelerated SoC. The effort for IP integration is comparable to using a software library, hence, providing a significant advantage over a manual IP integration.

SUMMARYAutonomous multi-agent systems show promise in countless applications, but can be hindered in environments where inter-agent communication is limited. In such cases, this paper considers a scenario where agents communicate intermittently through a cloud server. We derive a graph transformation mapping the kernel of a graph's Laplacian to a desired configuration vector while retaining graph topology characteristics. The transformation facilitates derivation of a self-triggered controller driving agents to prescribed configurations while regulating instances of inter-agent communication. Experimental validation of the theoretical results shows the self-triggered approach drives agents to a desired configuration using fewer control updates than traditional periodic implementations.

The authors present a new method for creating a graph database schema (GDBS) based on an entity-relationship diagram (ERD) of the application domain, which is mapped to a GDBS in a two-step process. First, the original ERD is adjusted to a semantically equivalent ERD (enabling it to be mapped in step two). In the second step, the adjusted ERD is mapped to a GDBS according to specific rules. The resulting GDBS includes integrity constraints that enrich existing graph databases.

While developing concurrent systems, one of the important properties to be checked is deadlock freedom. Model checking is an accurate technique to detect errors, such as deadlocks. However, the problem of model checking in complex software systems is state space explosion in which all reachable states cannot be generated due to exponential memory usage. When a state space is too large to be explored exhaustively, using meta-heuristic and evolutionary approaches seems a proper solution to address this problem. Recently, a few methods using genetic algorithm, particle swarm optimization and similar approaches have been proposed to handle this problem. Even though the results of recent approaches are promising, the accuracy and convergence speed may still be a problem. In this paper, a novel method is proposed using Bayesian Optimization Algorithm (BOA) to detect deadlocks in systems specified formally through graph transformations. BOA is an Estimation of Distribution Algorithm in which a Bayesian network (as a probabilistic model) is learned from the population and then sampled to generate new solutions. Three different structures are considered for the Bayesian network to investigate deadlocks in the benchmark problems. To evaluate the efficiency of the proposed approach, it is implemented in GROOVE, an open source toolset for designing and model checking graph transformation systems. Experimental results show that the proposed approach is faster and more accurate than existing algorithms in discovering deadlock states in the most of case studies with large state spaces.

In analysis of ubiquitous networks, one critical work is to understand the internal structure of the networks. Many approaches are proposed to address the structure mining in the graph. Unfortunately, these approaches cannot cope with the big graph generated by large-scale streaming data. Aiming to mine the structure from the big graph, this paper presents an efficient mining framework, namely cSketch, which is used for capturing the cliques from big graph quickly. Two illustrative examples are conducted for demonstrating the feasibility and effectiveness of the proposed framework.

Graph grammars may be used to formally describe computational systems, modeling the states as graphs and the possible state changes as rules (whose left- and right-hand sides are graphs). The behavior of the system is defined by the application of these rules to the state-graphs. From a practical point of view, the extension of rules to enable description of extra conditions that must be satisfied upon rule application is highly desirable. An example is the specification of negative application conditions, or NACs, that describe situations that prevent the application of a rule. This extension of the basic formalism enhances the expressiveness of rules, generally allowing simpler specifications. Another extension that is fundamental for practical applications is the possibility to use data types, like natural numbers, lists, etc., as attributes of graphical elements (vertices and edges). Attributed graph grammars are well-investigated and used. However, there is a lack of verification techniques for this kind of grammar mainly due to the fact that data types are typically infinite domains, and thus techniques like model checking can not be used directly (without abstraction constructions). The present work provides a theoretical foundation for theorem proving graph grammars with negative application conditions and attributes. This is achieved by generating an event-B model from a graph grammar. Event-B models are composed by sets and axioms to define types, and by states and events to describe behavior. After constructing the event-B model that is semantically equivalent to a graph grammar, properties about reachable states may be proven using the various theorem provers available for event-B in the Rodin platform. This strategy allows the verification of systems with infinite-state spaces without using any kind of approximation.

Design patterns are strategies for solving commonly occurring problems within a given context in software design. In the process of re-engineering, detection of design pattern instances from source codes can play a major role in understanding large and complex software systems. However, detecting design pattern instances is not always a straightforward task. In this paper, based on the graph theory, a new design pattern detection method is presented. The proposed detection process is subdivided into two sequential phases. In the first phase, we concern both the semantics and the syntax of the structural signature of patterns. To do so, the system under study and the patterns asked to be detected, are transformed into semantic graphs. Now, the initial problem is converted into the problem of finding matches in the system graph for the pattern graph. To reduce the exploration space, based on a predetermined set of criteria, the system graph is broken into the possible subsystem graphs. After applying a semantic matching algorithm and obtaining the candidate instances, by analyzing the behavioral signature of the patterns, in the second phase, final matches will be obtained. The performance of the suggested technique is evaluated on three open source systems regarding precision and recall metrics. The results demonstrate the high efficiency and accuracy of the proposed method.

Fuzzy graph structures have applications in different fields, including environmental science, social science, geography and linguistics. A single-valued neutrosophic graph structure is a generalization of fuzzy graph structure. In this research paper, we first introduce the notion of single-valued neutrosophic graph structures. We present certain operations of single-valued neutrosophic graph structures. We elaborate these operations with examples. Further, we discuss some novel applications of single-valued neutrosophic graph structures in decision-making problems. Finally, we present our developed methods by algorithms.

Locally-biased graph algorithms are algorithms that attempt to find local or small-scale structure in a large data graph. In some cases, this can be accomplished by adding some sort of locality constraint and calling a traditional graph algorithm; but more interesting are locally-biased graph algorithms that compute answers by running a procedure that does not even look at most of the input graph. This corresponds more closely to what practitioners from various data science domains do, but it does not correspond well with the way that algorithmic and statistical theory is typically formulated. Recent work from several research communities has focused on developing locally-biased graph algorithms that come with strong complementary algorithmic and statistical theory and that are useful in practice in downstream data science applications. We provide a review and overview of this work, highlighting commonalities between seemingly-different approaches, and highlighting promising directions for future work., Comment: 19 pages, 13 figures

Graph processing is becoming a crucial component for analyzing big data arising in many application domains such as social and biological networks, fraud detection, and sentiment analysis. As a result, a number of computational models for graph analytics have been proposed in the literature to help users write efficient large scale graph algorithms. In this paper we present an alternative model for implementing graph algorithms using a linear algebra based specification. We first specify a set of linear algebra primitives that allows users to express graph algorithms by composition of linear algebra operations. We then describe a high performance implementation of these primitives using C $$++$$ and subsequently its integration with the Spark framework to achieve the scalability we need for large systems. We provide an overview of our implementation and also compare and contrast the expressiveness and performance of various algorithms implemented with our approach with that of the current Spark GraphX implementation of those algorithms.

One thing that is still being developed for graph databases is integrity constraint (IC) support. One possibility to IC proposal is to consider a graph conceptual schema and a graph database schema. At least inherent ICs coming from a graph conceptual schema should be considered as explicit ICs on the graph databases level, i.e., using a DDL. In the paper, we focus on graph database Neo4j and its possibilities to express a database schema and ICs. We extend these possibilities through new constructs in Neo4j DDL including their prototype implementation and experiments.

Graph-rewriting is a promising computation model for computer-aided design (CAD) applications that operate on graph-based design models. Graph-rewriting-based CAD systems rely on predefined production rules. These rules encode the set of possible actions that may be taken within the design process to make changes to the current design. This paper presents a method for automatically inducing new production rules from existing sample designs. The methods applicability is illustrated in context of conceptual spacecraft design. Results gained from experiments, where existing rules were deliberately left out and had to be rediscovered, show that the induced rules are often similar or identical to the original rules.

We propose a new approach for modelling the process of RNA folding as a graph transformation guided by the global value of free energy. Since the folding process evolves towards a configuration in which the free energy is minimal, the global behaviour resembles the one of a self-adaptive system. Each RNA configuration is a graph and the evolution of configurations is constrained by precise rules that can be described by a graph grammar., In Proceedings GaM 2016, arXiv:1612.01053

Graph rewrite formalisms are a powerful approach to modeling complex molecular systems. They capture the intrinsic concurrency of molecular interactions, thereby enabling a formal notion of mechanism (a partially ordered set of events) that explains how a system achieves a particular outcome given a set of rewrite rules. It is then useful to verify whether the mechanisms that emerge from a given model comply with empirical observations about their mutual interference. In this work, our objective is to determine whether a specific event in the mechanism for achieving X prevents or promotes the occurrence of a specific event in the mechanism for achieving Y. Such checks might also be used to hypothesize rules that would bring model mechanisms in compliance with observations. We define a rigorous framework for defining the concept of interference (positive or negative) between mechanisms induced by a system of graph-rewrite rules and for establishing whether an asserted influence can be realized given two mechanisms as an input., In Proceedings CREST 2018, arXiv:1901.00073

In recent years, the increased interest in application areas such as social networks has resulted in a rising popularity of graph-based approaches for storing and processing large amounts of interconnected data. To extract useful information from the growing network structures, efficient querying techniques are required.

This paper describes the graph transfor-mation system (GT System) for SemEval 2019 Task 1: Cross-lingual Semantic Parsing with Universal Conceptual Cognitive Annotation (UCCA)1. The input of GT System is a pair of text and its unannotated xml, which is a layer 0 part of UCCA form. The output of GT System is the corresponding full UCCA xml. Based on the idea of graph illustration and transformation, we perform four main tasks when building GT System. At the first task, we illustrate the graph form of stanford dependencies2 of input text. We then transform into an intermediate graph in the second task. At the third task, we continue to transform into ouput graph form. Finally, we create the output UCCA xml. The evaluation results show that our method generates good-quality UCCA xml and has a meaningful contribution to the semantic represetation sub-field in Natural Language Processing.

The Double Pushout (DPO) approach for graph transformation naturally allows an abstraction level of biochemical systems in which individual atoms of molecules can be traced automatically within chemical reaction networks. Aiming at a mathematical rigorous approach for isotopic labeling design we convert chemical reaction networks (represented as directed hypergraphs) into transformation semigroups. Symmetries within chemical compounds correspond to permutations whereas (not necessarily invertible) chemical reactions define the transformations of the semigroup. An approach for the automatic inference of informative labeling of atoms is presented, which allows to distinguish the activity of different pathway alternatives within reaction networks. To illustrate our approaches, we apply them to the reaction network of glycolysis, which is an important and well understood process that allows for different alternatives to convert glucose into pyruvate.