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.