An Online Model Checking Tool for Safety and Liveness Bugs

Modern software model checkers are usually used to find safety violations. However, checking liveness properties can offer a more natural and effective way to detect errors, particularly in complex concurrent and distributed e-business systems. Specifying global liveness properties which should always eventually be true proves to be more desirable, but it is hard for existing software model checkers to verify liveness in real codes because doing so requires finding an infinite execution. For solving such a challenge,this paper proposes an online checking tool to verify the safety and liveness properties of complex systems. We adopt the linear temporal logic to describe the semantics of the finite model checking, use binary instrumentation to obtain the distribute states and apply a checking engine to dynamically verify the finite trace linear temporal logic properties. At last, we demonstrate the method in a distributed system using distributed protocol Paxos and achieve good results by experiments.

By: Zhengwei Qi; Liang Liu; Alei Liang; Hao Wang; Ying Chen

Published in: IEEE International Conference on Parallel and Distributed Systems, Australia, IEEE, p.493-500 in 2008

Please obtain a copy of this paper from your local library. IBM cannot distribute this paper externally.

Questions about this service can be mailed to .