Advertisement
Published in:
2006 | OriginalPaper | Chapter
CTL Model Checking for Boolean Program
Authors : Taehoon Lee, Gihwon Kwon, Hyuksoo Han
Published in: Computational Science and Its Applications - ICCSA 2006
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.