Model checking has attracted considerable attention since this technique is an automatic technique for verifying finite state concurrent systems. It is a formal method to verify if a software system or hardware system meets its properties. Nowadays, model checkers have become indispensable tools in hardware and software design and implementation, since they can reduce human efforts. Time and feasibility of the model checking process depends up on the size and complexity of the formal system model. However, the state space explosion problem still remains a major hurdle, as the number of global states can be enormous. There are many methods to improve the speed of model checkers and abstraction technology is one of them. Abstraction amounts to removing or simplifying details, as well as removing entire components of the concrete model irrelevant to the specifications. In practice, abstraction-based methods have been essential to verify designs of different fields of industrial complexity. Manual abstraction is ad hoc and error-prone; hence, automatic abstraction strategies are desirable for verifying actual hardware and software design.

This thesis presents a new approach to check the model using two abstractions---Universal Abstraction and Existential Abstraction. These new techniques can check both the Existential fragment of Computational Tree Logic (ECTL) and the Universal fragment of Computational Tree Logic (ACTL) specifications. I developed a Model Checker, called LOTUS, building upon these new techniques with a traditional fixed point algorithm on Linux. Experimental results confirmed the feasibility and validity of this new dynamic model checking technique. The input grammar is designed and implemented using Bison and YACC on Linux. The process for this new technique follows. First, automatically construct two abstraction models according to the specifications defined in the input file by the user. Second, LOTUS verifies whether the abstraction model satisfies the specifications and outputs the conclusion. Lotus can produce the final output, if the conclusion is credible; otherwise, refine the two abstraction models according to the counterexamples or witnesses produced by the abstraction model. This process is repeated until the abstraction model is equivalent to the concrete model or the authentic conclusion can be obtained. In this thesis, I aim to provide a complete picture of this dynamic model-checking algorithm, ranging from design details to implementation-related issues and experiments of the Philosopher Dinning Problem.

The main contributions of this approach include three aspects. First, Dynamic Abstraction Algorithm can check both ECTL and ACTL within abstraction methods. Second, a transition abstraction is introduced in this thesis with the purpose is to make the model checker easier to implement. Third, refinement of both abstraction models according to either witness or counterexample is actually modifying the transitions. This method may reduce time and space consumption.