CTL Property Language in Formal Verification of Systems A System Approach

Abstract: We use symbolic model checking to verify a VHDL design. This paper mainly focuses on Computational Tree Logic (CTL) for model checking problem. We have explained these two terms “CTL” and “model checking ” for providing a clear idea about these two. Most importantly we have explored the ways of uses of CTL formulae in the case of model checking. The importance of the model checking, the ways of specifying properties in CTL and some most commonly used CTL formulae in checking are also stated. Also the uses and importance of fairness constraints in CTL formula and the conversion of CTL operators have also been included in this paper. Lastly, we have given an example of the processes of model checking.