Proven: A Graphical Tool for Model-Checking Function Block Diagrams

Abstract

Model checking as a verification method has the benefit of exhaustive coverage. As checked properties can also exclude unwanted behavior, model checking has been shown to reveal hidden design issues in instrumentation and control (I&C) systems already subjected to more conventional verification techniques. However, one reason why the perceived cost of formal verification can be seen as high is the lack of established, user-friendly, domain-specific tools. In this paper, we introduce a new graphical tool called Proven for the model-checking of I&C logics programmed with function block diagrams, based on the popular open-source symbolic model checker NuSMV. We describe Proven's functions, its implementation, novel features, and our ideas for its further development. Proven can be used to verify non-standard vendor-specific block diagrams, as well as more generic functional diagrams used in various Systems Engineering activities.