Wednesday, March 4, 2020

STATE SPACE GENERATION FRAMEWORK BASED ON BINARY DECISION DIAGRAM FOR DISTRIBUTED EXPLICIT MODEL CHECKING


Author :  Nacer Tabib

Affiliation :  Constantine 2 University

Country :  Algeria

Category :  Computer Science & Information Technology

Volume, Issue, Month, Year :  6, 1, November, 2016

ABSTRACT

This paper proposes a new framework based on Binary Decision Diagrams (BDD) for the graph distribution problem in the context of explicit model checking. The BDD are yet used to represent the state space for a symbolic verification model checking. Thus, we took advantage of high compression ratio of BDD to encode not only the state space, but also the place where each state will be put. So, a fitness function that allows a good balance load of states over the nodes of an homogeneous network is used. Furthermore, a detailed explanation of how to calculate the inter-site edges between different nodes based on the adapted data structure is presented.

Keyword :  Graph distribution, Binary Decision Diagram, State space generation, Formal verification, Model Checking.

For More Details  :  https://airccj.org/CSCP/vol6/csit64825.pdf


No comments:

Post a Comment