Volume 20, Issue 2 (9-2023)
JSDP 2023, 20(2): 175-194 |
Back to browse issues page
Download citation:
BibTeX | RIS | EndNote | Medlars | ProCite | Reference Manager | RefWorks
Send citation to:
BibTeX | RIS | EndNote | Medlars | ProCite | Reference Manager | RefWorks
Send citation to:
partabian J. Checking reachability property of systems specified through graph transformation with the approach of discovery conditional dependency between the rules. JSDP 2023; 20 (2) : 11
URL: http://jsdp.rcisp.ac.ir/article-1-1240-en.html
URL: http://jsdp.rcisp.ac.ir/article-1-1240-en.html
Abstract: (304 Views)
Model checking is among the most effective techniques for automatic verification of hardware and software systems’ properties. Generally, in this method, a model of the desired system is generated and all possible states are explored in the space state graph to find errors and undesirable patterns. In models of large and complex systems, if the size of the generated state space is too extensive so that not all available states can be explored due to computational restrictions, the problem of state space explosion occurs. In fact, this problem confines the validation process in model verification systems. To use the model checking technique, the system must be described in a formal language. Graphs are very beneficial and intuitive tools for describing and modeling software systems. Correspondingly, graph transformation system provides a proper tool for formal description of software system features as well as their automatic verification.
Various techniques have been investigated in the researches to reduce the effect of state space explosion problem in the model checking process. Some of these methods try to reduce the required memory by reducing the number of cases explored. Among others are symbolic model checking, partial-order reduction, symmetry reduction, and scenario-driven model checking. In a complex system, these algorithms, along with conventional methods such as DFS or BFS search algorithms may not afford any complete answer due to the explosion of state space. Hence, the use of intelligent methods such as knowledge-based techniques, datamining, machine learning, and meta-heuristic algorithms which do not entail full state space exploration could be advantageous.
Recent researches attest that exploring the state space using intelligent methods could be a promising idea. Therefore, an intelligent method is used in this research to explore the state space of large and complex systems. Accordingly in this paper, first a model of the desired system is created using graph conversion system. Then a portion of the state space of the model is generated. Afterwards, using the conditional probability table, the dependencies between the rules in the paths toward the goal state are discovered. Finally, by means of the discovered dependencies, the rest of the model state space is intelligently explored. In other words, only promising paths, i.e. those who match the detected dependencies are explored to reach the goal state. It is worth noting that the first goal of the proposed approach is to find a goal state, i.e., one in which either the safety property is violated or the reachability property is satisfied in the shortest possible time. The second less important goal is to reduce the number of explored states in the graph of the state space until reaching the goal state. This paper provides a way to check the availability feature in complex and large software systems modeled in the official graph transformation language. The suggested method is implemented in GROOVE which is an open source toolset for designing and model checking graph transformation systems. The results of experimental tests indicate that the proposed approach is faster than the previous methods and produces a shorter counterexample/witness.
Various techniques have been investigated in the researches to reduce the effect of state space explosion problem in the model checking process. Some of these methods try to reduce the required memory by reducing the number of cases explored. Among others are symbolic model checking, partial-order reduction, symmetry reduction, and scenario-driven model checking. In a complex system, these algorithms, along with conventional methods such as DFS or BFS search algorithms may not afford any complete answer due to the explosion of state space. Hence, the use of intelligent methods such as knowledge-based techniques, datamining, machine learning, and meta-heuristic algorithms which do not entail full state space exploration could be advantageous.
Recent researches attest that exploring the state space using intelligent methods could be a promising idea. Therefore, an intelligent method is used in this research to explore the state space of large and complex systems. Accordingly in this paper, first a model of the desired system is created using graph conversion system. Then a portion of the state space of the model is generated. Afterwards, using the conditional probability table, the dependencies between the rules in the paths toward the goal state are discovered. Finally, by means of the discovered dependencies, the rest of the model state space is intelligently explored. In other words, only promising paths, i.e. those who match the detected dependencies are explored to reach the goal state. It is worth noting that the first goal of the proposed approach is to find a goal state, i.e., one in which either the safety property is violated or the reachability property is satisfied in the shortest possible time. The second less important goal is to reduce the number of explored states in the graph of the state space until reaching the goal state. This paper provides a way to check the availability feature in complex and large software systems modeled in the official graph transformation language. The suggested method is implemented in GROOVE which is an open source toolset for designing and model checking graph transformation systems. The results of experimental tests indicate that the proposed approach is faster than the previous methods and produces a shorter counterexample/witness.
Article number: 11
Keywords: Model checking, State space explosion, Graph transformation system, Conditional probability table, Reachability property
Type of Study: Research |
Subject:
Paper
Received: 2021/06/10 | Accepted: 2023/06/2 | Published: 2023/10/22 | ePublished: 2023/10/22
Received: 2021/06/10 | Accepted: 2023/06/2 | Published: 2023/10/22 | ePublished: 2023/10/22
Send email to the article author
| Rights and permissions | |
 |
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License. |
