Preliminary results are presented of a comparison made between a model cheeking 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 Büchi automaton. Numerical results show a better performance of our tool for domains of up to 103 states.
CITATION STYLE
García, F., & Sánchez, A. (2006). Formal verification of safety and liveness properties for logic controllers. A tool comparison. In 2006 3rd International Conference on Electrical and Electronics Engineering. https://doi.org/10.1109/ICEEE.2006.251867
Mendeley helps you to discover research relevant for your work.