Fuzzy Genetic Algorithm Approach for Verification of Reachability and Detection of Deadlock in Graph Transformation Systems

EasyChair Preprint no. 4327

Abstract

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.

Keyphrases: deadlock, Fuzzy Genetic Algorithm, model checking, reachability property

@Booklet{EasyChair:4327,
  author = {Nahid Salimi and Vahid Rafe and Hamed Tabrizchi and Amir Mosavi},
  title = {Fuzzy Genetic Algorithm Approach for Verification of Reachability and Detection of Deadlock in Graph Transformation Systems},
  howpublished = {EasyChair Preprint no. 4327},

  year = {EasyChair, 2020}}