Abstract Effective test case generation is crucial for ensuring software correctness, whereas generating high-coverage test suites efficiently remains a challenge. Graph transformations provide a formal way to specify and analyse software systems by modeling system operations as transformation rules and constructing a state-based representation of system behavior. Model-based testing (MBT) often uses model checking over this representation to discover execution paths that satisfy certain test requirements. However, such approaches suffer from severe scalability issues due to the rapid growth of the state space and the high computational cost of exhaustive exploration. While optimization-based approaches mitigate these issues by exploring a reduced portion of the state space, they still struggle to scale effectively. MBT approaches using graph transformation faces the same scalability and often face additional challenges due to the richer structural complexity of graph-based models. However, apart from the behavioral information derived from state transitions, graph transformation systems also encode explicit structural relationships between states and transformation rules. These structural characteristics can be used to define and evaluate test objectives. To exploit this, we propose a novel approach based on deep reinforcement learning to generate test suites for systems specified through graph transformations. We use the reward/penalty mechanism of reinforcement learning to optimize the selection of moves within the state space, enabling the generation of test cases based on prior decisions. Our goal is to achieve greater coverage of test objectives while minimizing the size of the test cases. The method has been implemented in GROOVE, an open-source toolset for designing and model checking graph transformation systems. Experimental results on well-known case studies demonstrate that our approach achieves higher coverage with reduced computational cost compared to state-of-the-art techniques.

Abstract Bug localization (BL) is known as one of the major steps in the program repair process, which generally seeks to find a set of commands causing a program to crash or fail. At the present time, locating bugs and their sources quickly seems to be impossible as the complexity of modern software development and scaling is soaring. Accordingly, there is a huge demand for BL techniques with minimal human intervention. A graph representing source code typically encodes valuable information about both the syntactic and semantic structures of programs. Many software bugs are associated with these structures, making graphs particularly suitable for bug localization (BL). Therefore, the key contributions of this work involve labeling graph nodes, classifying these nodes, and addressing imbalanced classifications within the graph data structure to effectively locate bugs in code. A graph-based bug classifier is initially introduced in the method proposed in this paper. For this purpose, the program source codes are mapped to a graph representation. Since the graph nodes do not have labels, the Gumtree algorithm is then exploited to label them by comparing the buggy graphs and the corresponding bug-free ones. Afterward, a trained, supervised node classifier, developed based on a graph neural network (GNN), is applied to classify the nodes into buggy or bug-free ones. Given the imbalance in the data, accuracy, precision, recall, and F1-score metrics are used for evaluation. Experimental results on identical datasets show that the proposed method outperforms other related approaches. The proposed approach effectively localizes a broader spectrum of bug types, such as undefined properties, functional bugs, variable naming errors, and variable misuse issues .

The advent of computer networks makes network protocols — running on this unprotected environment — vulnerable against various attacks and malefactions. Hence, methods for automatic security verification of protocols in the early stages of protocol design are absolutely required and cause efficiency and security enhancement. Much work has been carried out in the context of protocol vulnerability analysis using model checking, but most of them focus on security protocols that aim to provide data security and integrity, whereas there are other communication network protocols, that need a specific level of security and have their own safety characteristics. These kinds of network protocols often send some control packets and use the timing information to obtain the appropriate degree of security. However, time is abstracted away in most proposed methods for protocol vulnerability analysis to avoid state space explosion. Therefore, it is not possible to verify timing behaviors. In this article, we propose timed automata-based method for formal verification of network protocols' security properties with the appropriate abstraction level. We apply our method to analyze Mobile Internet Protocol version 6 and show how to avoid state space explosion using time concepts in the protocol model. Copyright © 2015 John Wiley & Sons, Ltd.

Cloud computing is a relatively new concept in the distributed systems and is widely accepted as a new solution for high performance and distributed computing. Its dynamisms in providing virtual resources for organisations and laboratories and its pay-per-use policy make it very popular. A workflow models a process consisting of a series of steps that shape an application. Workflow scheduling is the method for assigning each workflow task to a processing resource in a way that specific workflow rules are satisfied. Some scheduling algorithms for workflows may assume some quality of service parameter such as cost and deadline. Some efforts have been done on workflow scheduling on cloud computing environments with different service level agreements. But most of them suffer from low speed. Here, we introduce a new hybrid heuristic algorithm based on particle swarm optimisation (PSO) and gravitation search algorithms. The proposed algorithm, in addition to processing cost and transfer cost, takes deadline limitations into account. The proposed workflow scheduling approach can be used by both end-users and utility providers. The CloudSim toolkit is used as a cloud environment simulator and the Amazon EC2 pricing is the reference pricing used. Our experimental result shows about 70% cost reduction, in comparison to non-heuristic implementations, 30% cost reduction in comparison to PSO, 30% cost reduction in comparison to gravitational search algorithm and 50% cost reduction in comparison to hybrid genetic-gravitational algorithm.

The usually heterogeneous and decentralized nature of entities in the service-oriented architecture has paved the ground for the implementation of approaches distributed according to the constantly changing needs of business. Also, as the distribution of entities and processes increases, the need to provide security over software and hardware sources, which have reached the public thanks to an open space as a result of the service-oriented architecture, is felt. Therefore, security modeling at the level of service-oriented architecture can boost system reliability and enhance its stability once applied and employed. This research provides a secure framework through which to develop software based on the service-oriented architecture. The proposed framework has been modeled using the SoaML profile, which has been introduced for modeling service-oriented environments. The framework's security aspects have been tested by the modeling and specification language Alloy, which is based on the first-order logic. Its accuracy has also been well investigated. Tapping into the model-driven development, this framework can provide an answer to existing security challenges for service-oriented architecture software. Copyright © 2015 John Wiley & Sons, Ltd.

Graph transformation is a general visual modeling language which is suitable for stating the dynamic semantics of the designed models formally. We present a highly understandable yet precise approach to formally define the behavioral semantics of UML 2.0 Activity diagrams by using graph transformation. In our approach we take into account control flow and data flow semantics. Our proposed semantics is based on token-like semantics and traverse-to-completion. The main advantage of our approach is automated formal verification and analysis of UML Activities. We use AGG to design Activities and we use our previous approach to model checking graph transformation system. Hereby, designers can verify and analyze designed Activity diagrams. Since workflow modeling is one of the main application areas of the Activities, we use our proposed semantics for modeling and verification of workflows to illustrate our approach.

Today, it's an important requirement to have software systems without any bug. Model checking has proven to be a viable solution for reasoning about behavior properties of many different software artifacts. In this paper, we present a solution to verify software models which formally specified by layered graph transformation systems using a model checker called Bogor.

Nowadays, using of Service-Oriented Architectures (SOA) is spreading as a flexible architecture for developing dynamic enterprise systems.In this paper we investigate fault tolerance mechanisms for modeling services in service-oriented architecture. We propose a metamodel (formalized by a type graph) with graph rules for monitoring services and their communications to detect existing faults.

Graph Grammars have recently become more and more popular as a general formal modeling language. Behavioral modeling of dynamic systems and model to model transformations are a few well-known examples in which graphs have proven their usefulness in software engineering. A special type of graph transformation systems is layered graphs. Layered graphs are a suitable formalism for modeling hierarchical systems. However, most of the research so far concentrated on graph transformation systems as a modeling means, without considering the need for suitable analysis tools. In this paper we concentrate on how to analyze these models. We will describe our approach to show how one can verify the designed graph transformation systems. To verify graph transformation systems we use a novel approach: using Bogor model checker to verify graph transformation systems. The AGG-like graph transformation systems are translated to BIR — the input language of Bogor — and Bogor verifies that model against some properties defined by combining LTL and special purpose graph rules. Supporting schema-based and layered graphs characterize our approach among existing solutions for verification of graph transformation systems.

The CORBA Component Model (CCM) middleware provides a standard way to configure, manage and deploy distributed components. However, some current implementation of CCM is flawed with unreasonable communication overhead when components are in the same address space. Previous attempts to alleviate this drawback have tried to provide mechanisms for direct local communication of such components, but have sacrificed ORB services all together. Since such components do not communicate through ORB. They are deprived from ORB services such as events and naming. In case of need, programmers should implement such services themselves. This paper presents an alternative approach that likewise eliminates the unnecessary communication overhead between local components, but in addition provides them with local ORB-like services. A unit inside each container is made responsible for directing the communications between components within or outside the container. In case of local communications, requests are passed to the local components without ORB involvement. ORB-like services, namely events and naming, are provided by this unit locally for local components. Implementation results of the proposed approach with local event and naming services support show a favorable reduction of local communication overheads