CTL model checking for boolean program

Abstract

Nowadays, there are some subtle errors in a software system, So verification technique is very important, The one of important verification technique is model checking technique, Model checking is a technique to verify behavior of system with desired property, There are many researches about software model checking, As a result, predicate abstraction techniques are proposed and many tools for C or Java are developed. In general, there are two types of properties: The first is the safety properties. And other one is liveness properties. Most software model checking tools can only verify safety properties, In this paper, we describe CTL model checking algorithm based on Boolean program and describe model checking tool for Simple Java program which used in Lego robot to verify liveness property. Our model checking tool can check not only safety property but also liveness property and we describes case study verifying safety property and liveness property of LEGO robot. © Springer-Verlag Berlin Heidelberg 2006.