A meta-heuristic solution for automated refutation of complex software systems specified through graph transformations

One of the best approaches for verifying software systems (especially safety critical systems) is the model checking in which all reachable states are generated from an initial state. All of these states are searched for errors or desirable patterns. However, the drawback for many real and complex systems is the state space explosion in which model checking cannot generate all the possible states. In this situation, designers can use refutation to check refusing a property rather than proving it. In refutation, it is very important to handle the state space for finding errors efficiently. In this paper, we propose an efficient solution to implement refutation in complex systems modeled by graph transformation. Since meta-heuristic algorithms are efficient solutions for searching in the problems with very large state spaces, we use them to find errors (e.g., deadlocks) in systems which cannot be verified through existing model checking approaches due to the state space explosion. To do so, we employ a Particle Swarm Optimization (PSO) algorithm to consider only a subset of states (called population) in each step of the algorithm. To increase the accuracy, we propose a hybrid algorithm using PSO and Gravitational Search Algorithm (GSA). The proposed approach is implemented in GROOVE, a toolset for designing and model checking graph transformation systems. The experiments show improved results in terms of accuracy, speed and memory usage in comparison with other existing approaches.     

Using Markov Chain Based Estimation of Distribution Algorithm for Model-Based Safety Analysis of Graph Transformation

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.     

Language-Emptiness Checking of Alternating Tree Automata Using Symbolic Reachability Analysis

Alternating tree automata and AND/OR graphs provide elegant formalisms that enable branching- time logics to be verified in linear time. The seminal work of Kupferman et al. [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. J. ACM, 47(2):312–360, 2000] showed that 1) branching-time model checking is reducible to the language non-emptiness checking of the product of two alternating automata representing the model and property under verification, and 2) the non-emptiness problem can be solved by performing a search on an AND/OR graph representing this product. Their algorithm, however, can only be implemented in an explicit-state model checker because it needs stacks to detect accept and reject runs. In this paper, we propose a BDD-based approach to check the language non-emptiness of the product automaton. We use a technique called “state recording” from Schuppan and Biere [Viktor Schuppan and Armin Biere. Efficient reduction of finite state model checking to reachability analysis. Int. Journal on Software Tools for Technology Transfer (STTT), 5(2–3):185–204, 2004] to emulate the stack mechanism from explicit-state model checking. This technique allows us to transform the product automaton into a well-defined AND/OR graph. We develop a BDD-based reachability algorithm to efficiently determine whether a solution graph for the AND/OR graph exists and thereby solve the model-checking problem. While “state recording” increases the size of the state space, the advantage of our approach lies in the memory saving BDDs can offer and the potential it opens up for optimisation of the reachability analysis. We remark that this technique always detects the shortest counter-example.     

Backward validation of communicating complex state machines in web services environments

Communicating Finite State Machines (CFSM) lack the high level syntactic and structural abstractions of Communicating Complex State Machines (CCSM), such as nesting and encapsulation, to model highly complex protocols that are likely to arise in web services environments. The incorporation of these features in a protocol specification model would require the design of a new validation technique to efficiently check for protocol errors, such as deadlocks and non-reachable transitions. A reachability graph is used to represent the execution states of the protocol and to verify their consistency. In this paper, we propose a new validation technique for protocols modeled with complex FSM, called RLRA (Reverse Leaping Reachability Analysis), which enables the detection of all deadlock errors. It is a backtracking approach, which first identifies an initial set of suspected states, those possibly containing deadlocks, then refines this set to those likely to cause deadlock, and finally backtracks through the graph while checking for errors until the root state of the protocol is reached. Leap graphs are employed to prune the number of execution states examined, and thereby mitigate the combinatorial explosion of the state space. Extensive tests and comparisons were performed, which show the effectiveness of our technique.     

Improving swarming using genetic algorithms

The verification of temporal properties against a given system may require the exploration of its full state space. In explicit model checking, this exploration uses a depth-first search and can be achieved with multiple randomized threads to increase performance. Nonetheless, the topology of the state space and the exploration order can cap the speedup up to a certain number of threads. This paper proposes a new technique that aims to tackle this limitation by generating artificial initial states, using genetic algorithms. Threads are then launched from these states and thus explore different parts of the state space. Our prototype implementation is 10% faster than state-of-the-art algorithms on a general benchmark and 40% on a specialized benchmark. Even if we expected a decrease in an order of magnitude, these results are still encouraging since they suggest a new way to handle existing limitations. Empirically, our technique seems well suited for “linear” topology, i.e., the one we can obtain when combining model checking algorithms with partial-order reduction techniques.

     

ProTest: An Automatic Test Environment for B Specifications

We present ProTest, an automatic test environment for B specifications. B is a model-oriented notation where systems are specified in terms of abstract states and operations on abstract states. ProTest first generates a state coverage graph of a B specification through exhaustive model checking, and the coverage graph is traversed to generate a set of test cases, each being a sequence of B operations. For the model checking to be exhaustive, some transformations are applied to the sets used in the B machine. The approach also works if it is not exhaustive; one can stop at any point in time during the state space exploration and generate test cases from the coverage graph obtained so far. ProTest then simultaneously performs animation of the B machine and the execution of the corresponding implementation in Java, and assigns verdicts on the test results. With some restrictions imposed on the B operations, the whole of the testing process is performed mechanically. We demonstrate the efficacy of our test environment by performing a small case study from industry. Furthermore, we present a solution to the problem of handling non-determinism in B operations.     

Formal testing of timed graph transformation systems using metric temporal graph logic

Embedded real-time systems generate state sequences where time elapses between state changes. Ensuring that such systems adhere to a provided specification of admissible or desired behavior is essential. Formal model-based testing is often a suitable cost-effective approach. We introduce an extended version of the formalism of symbolic graphs, which encompasses types as well as attributes, for representing states of dynamic systems. Relying on this extension of symbolic graphs, we present a novel formalism of timed graph transformation systems (TGTSs) that supports the model-based development of dynamic real-time systems at an abstract level where possible state changes and delays are specified by graph transformation rules. We then introduce an extended form of the metric temporal graph logic (MTGL) with increased expressiveness to improve the applicability of MTGL for the specification of timed graph sequences generated by a TGTS. Based on the metric temporal operators of MTGL and its built-in graph binding mechanics, we express properties on the structure and attributes of graphs as well as on the occurrence of graphs over time that are related by their inner structure. We provide formal support for checking whether a single generated timed graph sequence adheres to a provided MTGL specification. Relying on this logical foundation, we develop a testing framework for TGTSs that are specified using MTGL. Lastly, we apply this testing framework to a running example by using our prototypical implementation in the tool AutoGraph.

     

Saving Space by Fully Exploiting Invisible Transitions

Checking that a given finite state program satisfies a linear temporal logic property suffers from the state explosion problem. Often the resulting lack of available memory is more significant than any time limitations. One way to cope with this is to reduce the state graph used for model checking. We present an algorithm for constructing a state graph that is a projection of the program's state graph. The algorithm maintains the transitions and states that affect the truth of the property to be checked. Especially in conjunction with known partial order reduction algorithms, we show a substantial reduction in memory over using partial order methods alone, both in the precomputation stage, and in the result presented to a model checker. The price of the space reduction is a single additional traversal of the graph obtained with partial order reduction. As part of our space-saving methods, we present a new way to exploit Holzmann's Bit Hash Table, which assists us in solving the revisiting problem.     

Local Module Checking for CTL Specifications

Model checking is a well known technique for the verification of finite state models using temporal logic specification. While model checking is suitable for transformational systems (also called closed systems), it is unsuitable for open systems (also known as reactive systems) where the nondeterminism in the environment must be considered during verification. Module checking is an approach for the verification of open systems which have both closed (internal) and open (environment or external) states. It has been demonstrated in [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. Module checking. Information and Computation, 164:322–344, 2001] that the complexity of module checking branching time logic CTL is EXPTIME-complete. The approach to module checking is global and the method tries to establish that the property in question holds over all possible environments.This papers develops a local approach to CTL module checking using tableau rules. The proposed approach tries to determine a single environment under which the negation of the property is satisfied over the given module. Such a strategy, thus, leads to a local approach to module checking where we only explore states that are relevant to proving that the negation of the property can be satisfied over the given module using an appropriate witness (environment) that the algorithm also generates. While the worst case complexity of our algorithm is identical to the earlier complexity, we demonstrate that practical implementation of the proposed approach is feasible and yields much better results than the global approach.     

Networks of evolutionary processors: computationally complete normal forms

Networks of evolutionary processors (NEPs, for short) form a bio-inspired language generating computational model that was shown to be equivalent to the model of phrase-structure grammars. In this paper, we analyse different restricted variants of NEPs that preserve the computational power of the general model. We prove that any recursively enumerable language can be generated by a NEP where the derivation rules can be applied at arbitrarily chosen positions, the control of the communication is done by finite automata with at most three states, and either the rule sets are singletons or the underlying graph is a complete graph. If one uses networks with arbitrary underlying graphs and allows the additional application of insertions and deletions only to the right-most or the to left-most position of the derived words for some nodes, then we only need automata with only one state to control the communication in the network. Clearly, this result is optimal; moreover, finite automata with two states are necessary and sufficient in order to generate all the recursively enumerable languages when the derivation rules can be applied only at arbitrarily chosen positions.     

Towards an Integrated Graph Based Semantics for UML

Recently, we proposed an integrated formal semantics based on graph transformation for central aspects of UML class, object and state diagrams. In this paper, we explain the basic ideas of that approach and show how two more UML diagram types, sequence and collaboration diagrams, can be captured. For UML models consisting of a class diagram and particular state diagrams, a graph transformation system can be defined. Its graphs are associated with system states and its rules with operations in the class diagram and transitions in the state diagrams. Sequence and collaboration diagrams then characterize sequences of operation applications and therefore sequences of transformation rule applications. Thus valid sequence and collaboration diagrams correspond to derivations induced by the graph transformation system. Proceeding this way, it can be checked for example whether such an operation application sequence may be applied in a specific system state.     

Applications of graph grammar theory to consistency,synchronization and scheduling in data base systems

Graph grammar concepts are applied for the design of consistent states and manipulations modeling actions, transactions and schedules for simultaneous executions on data base systems. Especially we show how to use Church-Rosser Theorems for graph grammars to handle synchronization problems for data base systems in a multi-user environment. In this paper theses concepts are applied to a data base system for a library. For reasons of presentation the system is restricted to the basic features of a library but can be extended to more comfortable systems including also generalized data base systems. All manipulation rules are shown to preserve consistency and it is analysed exactly which of theses rules are collateral and for which of them further synchronization mechanisms are necessary. While consistent states are modelled as graphs and manipulation rules (resp. actions) as graph productions transactions correspond to sequences of productions, and schedules to sequences of parallel productions. The application of a schedule to a consistent state yields a “semantical schedule” which transforms the given state to some other state of the system. Sufficient conditions are given for a schedule to be consistent which means that consistent states are transformed into consistent states. Moreover we are able to define a degree of non-parallelism for schedules such that optimal schedules are those with minimal degree with respect to all equivalent ones. Applying results from graph grammar theory we are able to show that for each schedule there is a unique optimal one. A similar result is shown for semantical schedules where the semantical degree of non-parallelism is smaller than the syntactical one in general.     

Symbolic model checking for self-stabilizing algorithms

A distributed system is said to be self-stabilizing if it converges to safe states regardless of its initial state. In this paper we present our results of using symbolic model checking to verify distributed algorithms against the self-stabilizing property. In general, the most difficult problem with model checking is state explosion; it is especially serious in verifying the self-stabilizing property, since it requires the examination of all possible initial states. So far applying model checking to self-stabilizing algorithms has not been successful due to the problem of state explosion. In order to overcome this difficulty, we propose to use symbolic model checking for this purpose. Symbolic model checking is a verification method which uses Ordered Binary Decision Diagrams (OBDDs) to compactly represent state spaces. Unlike other model checking techniques, this method has the advantage that most of its computations do not depend on the initial states. We show how to verify the correctness of algorithms by means of SMV, a well-known symbolic model checker. By applying the proposed approach to several algorithms in the literature, we demonstrate empirically that the state spaces of self-stabilizing algorithms can be represented by OBDDs very efficiently. Through these case studies, we also demonstrate the usefulness of the proposed approach in detecting errors     

Bounded Model Checking Using Satisfiability Solving

The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verification in a highly automatic manner, and, thus, have attracted much interest in industry. Model checking programs are now being commercially marketed. However, model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in the number of system components. Much research has been devoted to ameliorating this problem.In this tutorial, we first give a brief overview of the history of model checking to date, and then focus on recent techniques that combine model checking with satisfiability solving. These techniques, known as bounded model checking, do a very fast exploration of the state space, and for some types of problems seem to offer large performance improvements over previous approaches. We review experiments with bounded model checking on both public domain and industrial designs, and propose a methodology for applying the technique in industry for invariance checking. We then summarize the pros and cons of this new technology and discuss future research efforts to extend its capabilities.     

UML状态机的模型检验方法

模型检验是一种确保设计规范正确性的形式化自动验证技术,本文提出了对UML状态机进行模型检验的方法。文中首先对UML状态机的语法和语义进行描述,然后基于语义中的RTC步给出生状态机全局可达状态迁移图的方法,方法的核心是在当前格局下根据使能条件确定所有的最大无冲突迁移集。文章最后给出算法以验证UML状态机是否满足用计算树逻辑（CTL）公式表示的性质。     

Extending C for Checking Shape Safety

The project Safe Pointers by Graph Transformation at the University of York has developed a method for specifying the shape of pointer-data structures by graph reduction, and a static checking algorithm for proving the shape safety of graph transformation rules modelling operations on pointer structures. In this paper, we outline how to apply this approach to the C programming language. We extend ANSI C with so-called transformers which model graph transformation rules, and with shape specifications for pointer structures. For the resulting language C-GRS, we present both a translation to C and and an abstraction to graph transformation. Our main result is that the abstraction of transformers to graph transformation rules is correct in that the C code implementing transformers is compatible with the semantics of graph transformation.     

Defining the abstract syntax of visual languages with advanced graph grammars—A case study based on behavior trees

Diagrammatic visual languages can increase the ability of engineers to model and understand complex systems. However, to effectively use visual models, the syntax and semantics of these languages should be defined precisely. Since most diagrammatic visual models that are currently used to specify systems can be described as (directed) typed graphs, graph grammars have been identified as a suitable formalism to describe the abstract syntax of visual modeling languages. In this article, we investigate how advanced graph-transformation techniques, such as conditional, structure-generic and type-generic graph-transformation rules, can help to improve and simplify the specification of the abstract syntax of a visual modeling language. To demonstrate the practicability of an approach that unifies these advanced graph-transformation techniques, we define the abstract syntax of behavior trees (BTs), a graphical specification language for functional requirements. Additionally, we provide a translational semantics of BTs by formalizing a translation scheme to the input language of the SAL model checking tool for each of the graph-transformation rules.     

On compliance checking for clausal constraints in annotated process models

Compliance management is important in several industry sectors where there is a high incidence of regulatory control. It must be ensured that business practices, as reflected in business processes, comply with the rules. Such compliance checks are challenging due to (1) the different life cycles of rules and processes, and (2) their disparate representations. (1) requires retrospective checking of process models. To address (2), we herein devise a framework where processes are annotated to capture the semantics of task execution, and compliance is checked against a set of constraints posing restrictions on the desirable process states. Each constraint is a clause, i.e., a disjunction of literals. If a process can reach a state that falsifies all literals of one of the constraints, then that constraint is violated in that state, and indicates non-compliance. Naively, such compliance can be checked by enumerating all reachable states. Since long waiting times are undesirable, it is important to develop efficient (low-order polynomial time) algorithms that (a) perform exact compliance checking for restricted cases, or (b) perform approximate compliance checking for more general cases. Herein, we observe that methods of both kinds can be defined as a natural extension of our earlier work on semantic business process validation. We devise one method of type (a), and we devise two methods of type (b); both are based on similar restrictions to the processes, where the restrictions made by methods (b) are a subset of those made by method (a). The approximate methods each guarantee either of soundness (finding only non-compliances) or completeness (finding all non-compliances). We describe how one can trace the state evolution back to the process activities which caused the (potential) non-compliance, and hence provide the user with an error diagnosis.