Formal verification of safety and liveness properties for logic controllers. a tool comparison

Preliminary results are presented of a comparison made between a model checking tool developed by our research group and Spin, a public domain model checking package. The theoretical fundaments of both tools are explicit model checking based on language emptiness. Using a simple example consisting of a set of logic controllers for driving the operation of pressurized tanks, we compare the computing performance of each stage in the model checking procedure for safety and liveness properties given as linear temporal logic (LTL) formulas. The controller ladder logic is modeled as a generalized Bilchi automaton. Numerical results show a better performance of our tool for domains of up to 10(3) states.