FBDVerifier: Interactive and Visual Analysis of Counter-example in Formal Verification of Function Block Diagram

Abstract

Model checking is often applied to verify safety-critical software implemented in programmable logic controller (PLC) language such as a function block diagram (FBD). Counter-examples generated by a model checker are often too lengthy and complex to analyze. This paper describes the FBDVerifier which allows domain experts to perform automated model checking and intuitive