Inductive model checking for state-based systems

Model checking has been proved a practical and effective technique for system verification. It explores the state space exhaustively to prove that a system behaves as expected by system designers. Although model checking has been proven in practice and has been used in the computing industry, it suffers from the state-space explosion problem. The problem concerns the fact that systems with a great number of states cannot be verified in reality due to a possibly gigantic state expansion in a limited space of hardware. Although many state space reduction techniques have been proposed to improve the state savings, they all have their own special cases in which the state explosion problem still exists. Until today researchers continue to study the problem and its final solutions.; This dissertation presents an inductive model checking (IMC) method, which combines the induction method and model checking, to improve the state savings for model checking. It applies the theory of induction to use model checking efficiently for system verification. IMC verifies a desired property against different atomic patterns (sequences of states) separately. Patterns are expanded and evaluated with model checking in the three steps of induction. In the basis step, patterns that start at the initial states are expanded to test the satisfaction of the desired property. In the hypothesis step, the property is assumed to have been satisfied with a specific number of continuous patterns. In the induction step, patterns that are connectable to the series of patterns assumed in the hypothesis are expanded with model checking to test the next satisfaction of the property. The verification results from these patterns are used to conclude the verification of the desired property.; Because the verification of a property is performed by verifying the property against different patterns separately, IMC needs less memory space for storing the states in these patterns. Moreover, IMC helps model checking to achieve a better space savings without conflicting with the other state-space reduction techniques used in the existing model checkers.