جستجوی مقالات مرتبط با کلیدواژه « model checking » در نشریات گروه « برق »

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.

The safety analysis of software systems, especially safety-critical ones, should be performed exactly because even a minor failure in these systems may result in disaster consequences. Also, such analysis must be done before implementation, i.e. the design step and in the model level. Model checking is an exact and mathematical-based way that gets a model of a system and analyzes it through exploring all reachable states of the model. Due to the complexity of some systems and their models, this way may face the state space explosion problem, i.e. it cannot explore all available states. A solution to solve this problem in these systems is that model checking tries to refute them, instead of verifying them, by finding errors such as deadlock (if available).Although, a heuristic has been previously proposed to find a deadlock in the model's state space and it has been applied in several simple heuristic search and evolutionary algorithms, its detection speed has been low. In this paper, we propose a novel heuristic to detect a deadlock in the model's state space, and test and compare its detection speed by applying it in several simple heuristic search algorithms such as iterative deepening A*, beam search, and evolutionary algorithms such as genetic, particle swarm optimization, and Bayesian optimization. Comparison results confirm that the new heuristic can detect a deadlock in less time than the previous heuristic.

One of the best solutions to verify software systems (especially critical systems) is model checking in which all reachable states are generated from an initial state and the generated state space is searched to find errors or some desirable patterns. However, the problem for many real and complex systems is the state space explosion in which model checking cannot generate all the states. In this paper, a solution is presented to cope with this problem in systems modeled by graph transformation. Since meta-heuristic algorithms are proper solutions to search in very large problem spaces, they employed in this research to find errors (e.g. deadlocks) in systems which cannot be verified through existing model checking approaches because of state space explosion problem. To do so, a Particle Swarm optimization (PSO) algorithm is empployed to consider only a subset of states (called population) in each step of the algorithm. To avoid local optima problem, PSO is combined with Gravitational Search Algorithm (GSA). Our proposed approach is implemented in GROOVE –a toolset for designing and model checking graph transformation system-. The experiments show better results in terms of accuracy, speed and memory usage in comparison with the existing approaches.