Evaluation of SAT-based Bounded Model Checking of ACTL Properties

Bounded model checking (BMC) based on SAT has been introduced as a complementary method to BDD-based symbolic model checking of LTL and ACTL properties in recent years. For general LTL and ACTL properties, BMC has traditionally aimed mainly at error detection, taking the advantage that error detection may only need to explore a small portion of the whole state space. Recently bounded model checking aiming at verification has also been proposed. The aim of this paper is to exploit the strength of BMC methods by combining different BMC approaches and compare it with the traditional BDD-based symbolic methods. We consider two bounded model checking methods, which are for error detection and verification of ACTL properties, respectively, and then combine them to a BMC algorithm. Based on this algorithm, we have implemented a tool named BMV (bounded model verifier), and carried out a number of experiments, and we have then compared BMV with Cadence SMV. The experimental results show tha...

• Type: Conference
• Year: 2007
• Where: TASE
• Authors: Yanyan Xu, Wei Chen, Liang Xu, Wenhui Zhang
• Keywords: ACTL Properties, Error Detection, Model Checking, Software Engineering, TASE 2007