Model checking analysis of observational transition system with SMV
Huaikou Miao · Jisuanji gongcheng yu sheji · 2008
Model checking is an important way in developing high confidence systems.A model checking method based on theorem proving is proposed,which describes the infinite system state by CafeOBJ and transfers a CafeOBJ specification to a finite SMV speci-fication,and its tool is implemented.By observing transition system shows that a counter example of a corresponding SMV specification is also a counter example of a CafeOBJ specification.It find errors lurked in systems at earlier stages of their development processes to avoid spending much money and time to correct errors later.