Using evolutionary algorithms for reachability analysis of complex software systems specified through graph transformation

2019 ◽  
Vol 191 ◽  
pp. 106577 ◽  
Author(s):  
Einollah Pira ◽  
Vahid Rafe ◽  
Amin Nikanjam
Keyword(s):  
Evolutionary Algorithms ◽  
Graph Transformation ◽  
Reachability Analysis ◽  
Software Systems

A NOVEL APPROACH TO VERIFY GRAPH SCHEMA-BASED SOFTWARE SYSTEMS

2009 ◽  
Vol 19 (06) ◽  
pp. 857-870 ◽  
Author(s):  
VAHID RAFE ◽  
ADEL T. RAHMANI
Keyword(s):  
Graph Transformation ◽  
Behavioral Modeling ◽  
Model Transformations ◽  
Software Systems ◽  
Hierarchical Systems ◽  
Input Language ◽  
Novel Approach ◽  
Graph Schema ◽  
Transformation Systems ◽  
Graph Transformation Systems

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.

Meta-Modelling and Graph Transformation for the Definition of Multi-View Visual Languages

2011 ◽  
pp. 74-101 ◽  
Author(s):  
Esther Guerra ◽  
Juan de Lara
Keyword(s):  
Whole Language ◽  
Model Simulation ◽  
Graph Transformation ◽  
Software Systems ◽  
Small Subset ◽  
Consistency Checking ◽  
Visual Languages ◽  
Meta Model ◽  
Definition Of ◽  
High Level

In this chapter, we present our approach for the definition of Multi-View Visual Languages (MVVLs). These are languages made of a set of different diagram types, which are used to specify the different aspects of a system. A prominent example of this kind of languages is UML, which defines a set of diagrams for the description of the static and dynamic elements of software systems. In the multi-view approach, consistency checking is essential to verify that the combination of the various system views yields a consistent description of the system. We use two techniques to define environments for MVVLs: meta-modelling and graph transformation. The former is used to describe the syntax of the whole language. In addition, we define a meta-model for each diagram type of the language (that we call viewpoint) as a restriction of the complete MVVL meta-model. From this high-level description, we can generate a customized environment supporting the definition of multiple system views. Consistency between views is ensured by translating each one of them into a unique repository model which is conformant to the meta-model of the whole language. The translation is performed by automatically generated graph transformation rules. Whenever a change is performed in a view, some rules are triggered to update the repository. These updates may trigger other rules to propagate the changes from the repository to the rest of the views. In our approach, graph transformation techniques are also used for other purposes, such as model simulation, optimization and transformation into other formalisms. In this chapter, we also discuss the integration of these concepts in the AToM3 tool, and show some illustrative examples by generating an environment for a small subset of UML.

scholarly journals Symbolic Analysis of Maude Theories with Narval

2019 ◽  
Vol 19 (5-6) ◽  
pp. 874-890
Author(s):  
MARÍA ALPUENTE ◽  
SANTIAGO ESCOBAR ◽  
JULIA SAPIÑA ◽  
DEMIS BALLIS
Keyword(s):  
Logic Programming ◽  
Reachability Analysis ◽  
Software Systems ◽  
Symbolic Computations ◽  
Fine Grained ◽  
Equational Unification ◽  
Symbolic Reasoning ◽  
Equational Theories ◽  
Graphical Tool ◽  
High Level

AbstractConcurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic software systems. Maude’s symbolic capabilities are based on equational unification and narrowing in rewrite theories, and provide Maude with advanced logic programming capabilities such as unification modulo user-definable equational theories and symbolic reachability analysis in rewrite theories. Intricate computing problems may be effectively and naturally solved in Maude thanks to the synergy of these recently developed symbolic capabilities and classical Maude features, such as: (i) rich type structures with sorts (types), subsorts, and overloading; (ii) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity; and (iii) classical reachability analysis in rewrite theories. However, the combination of all of these features may hinder the understanding of Maude symbolic computations for non-experienced developers. The purpose of this article is to describe how programming and analysis of Maude rewrite theories can be made easier by providing a sophisticated graphical tool called Narval that supports the fine-grained inspection of Maude symbolic computations.

Mapping Mobile Statechart Diagrams to the π-Calculus using Graph Transformation

2016 ◽  
Vol 12 (4) ◽  
pp. 1-20 ◽  
Author(s):  
Aissam Belghiat ◽  
Allaoua Chaoui
Keyword(s):  
Graph Transformation ◽  
Formal Semantics ◽  
Graph Grammar ◽  
Software Systems ◽  
Formal Approach ◽  
Agent Based ◽  
Modeling Simulation ◽  
Statechart Diagram ◽  
Automatic Mapping ◽  
Π Calculus

Mobile UML (M-UML) has been proposed as an extension of UML to model mobile agent-based software systems. As UML, M-UML suffers from lack of formal semantics due to its semi-formal nature which penalize the verification of correct behavior of the modeled systems. This paper provides a graphical yet formal approach for the modeling, simulation and verification of mobile statechart diagrams using graph transformations in the AToM3 tool. The authors have firstly proposed meta-models for mobile statechart diagram and flowgraph. Then, a twofold graph grammar is developed for the automatic mapping of mo-bile statechart diagrams into flowgraphs and in the same time generates the cor-responding p-calculus specification. This graph grammar enables either execu-tion through simulation by flowgraphs or verification through model checking, using existing tools (e.g. the Mobility Workbench, MWB). An illustrative example of the authors' approach is provided.

scholarly journals Fuzzy particle swarm optimization algorithm (NFPSO) for reachability analysis of complex software systems

2020 ◽  
Author(s):  
Nahid Salimi ◽  
Vahid Rafe ◽  
Hamed Tabrizchi ◽  
Amir Mosavi
Keyword(s):  
Model Checking ◽  
Evolutionary Algorithms ◽  
State Space ◽  
Heuristic Algorithms ◽  
Pso Algorithm ◽  
Software Systems ◽  
Adaptive Pso ◽  
Promising Solution ◽  
Speed And Accuracy ◽  
Fuzzy Adaptive

Nowadays, model checking is applied as an accurate technique to verify software systems. The main problem of model checking techniques is the state space explosion. This problem occurs due to the exponential memory usage by the model checker. In this situation, using meta-heuristic and evolutionary algorithms to search for a state in which a property is satisfied/violated is a promising solution. Recently, different evolutionary algorithms like GA, PSO, etc. are applied to find deadlock state. Even though useful, most of them are concentrated on finding deadlock. This paper proposes a fuzzy algorithm in order to analyze reachability properties in systems specified through GTS with enormous state space. To do so, we first extend the existing PSO algorithm (for checking deadlocks) to analyze reachability properties. Then, to increase the accuracy, we employ a Fuzzy adaptive PSO algorithm to determine which state and path should be explored in each step to find the corresponding reachable state. These two approaches are implemented in an open-source toolset for designing and model checking GTS called GROOVE. Moreover, the experimental results indicate that the hybrid fuzzy approach improves speed and accuracy in comparison with other techniques based on meta-heuristic algorithms such as GA and the hybrid of PSO-GSA in analyzing reachability properties.

Sign in / Sign up

Export Citation Format

Share Document