An Efficient LTL Model Checking Method for Large-Scale Systems

Abstract

The invention discloses a high-efficient LTL (Linear Temporal Logic) model detection method of large scale system. The LTL model detection method is characterized in that by adopting an LHS (Linear Hash Storage) algorithm, hash values stored in hash tables in a hard disc can be quickly found, and the hash tables can be stored in an outer memory by a new technique no matter whether the classification of the hash tables in an inner memory is empty or not, and the complexity of I / O (input / output) is the linearity size of the hash tables; by adopting a CDD (Cache Copy Detection) technique, a copy in the inner memory can be detected by effective accessing; by adopting HLS and CDD, the complexity of copy detection can be decreased; by adopting a DPM (dynamic path management) plan, the two embedded deep priority stacks can dynamically share an inner memory unit, and the jittering of the inner memory is solved by the effective stacking and state management, wherein the jittering of the inner memory refers to the frequent movement of the state in the inner memory, which may cause obvious increasing of I / O operation times, thereby reducing the algorithm efficiency.

Description

technical field [0001] The invention relates to the field of model detection, in particular to an LTL model detection technology. Background technique [0002] Model checking algorithm is a good method for formal verification of hardware and software. It can automatically detect whether the state of the system is satisfied and can detect counterexamples. Model checking is widely used in formal methods of hardware. But this method faces the problem of state space explosion, because the method will face insufficient memory when using large-scale systems. [0003] In practice, there are mainly two ways of model checking: [0004] In-memory algorithms and out-of-memory algorithms; in order to solve the state explosion problem, in-memory algorithms are mainly aimed at reducing the size and performance of the system. So far, there are many methods for memory algorithms, such as partial order reduction, symmetric reduction, abstraction extraction, combination extraction, symbolic...

AI Technical Summary

Problems solved by technology

So far, there are many methods for memory algorithms, such as partial order reduction, symmetric reduction, abstraction extraction, combination extraction, symbolic model detection, symbolic path tracing, automata theory, and boundary model detection, etc. However, due to memory In the large-scale system verification, the memory algorithm is not very practical

Images