A Heuristic Algorithm For Model-Checking Based On Counter Example Finding

Model-checking is one of the most successful automatic verification techniques in the past two decades. It has been used in the analysis and verification of finite-state systems such as sequential circuit designs and communication protocols. Because it is based on the exhaustive state space search, the state space explosion problem becomes the primary bottleneck when we apply model-checking to real systems.For systems with large state spaces, model checking technique may fail to finish the systems' verification due to the limitation of memory. On the other hand, random search algorithm could not find the potential errors effectively. In order to obtain a reasonable balance between memory usage and time expense, we present a possible solution based on heuristic information: we model the system as a Kripke structure and desired properties are expressed by LTL formulas. The LTL path formula in the negation of the original LTL formula describes the character of counter examples. Inspired by the idea of genetic algorithms, we proposed to use the "maximal structural complexity " of the subformulas satisfied in a path as heuristic information to guide the search direction. By case study, we demonstrate the heuristic algorithm can find the potential errors effectively and return responding diagnostic information, especially for large systems that are difficult to be verified by normal model-checking tool.The work includes:1.Designing the heuristic information based on Linear Temporal Logic, and some genetic operators, for example, select, across and mutate.2.Implementing prototypal tool based on the heuristic algorithm.3.Demonstrating the validation of the algorithm with a example...