User-friendly approach to formal verification
Proven is a graphical frontend for the popular open-source symbolic model checker NuSMV. It makes the formal verification of industrial control logics easy and fast. The application logic is modelled with a graphical diagram editor. The graphical model view is also used for the playback of counterexamples from NuSMV. As model checking is often an iterative process, the “model view” to counterexample animation is an essential benefit. Properties can be expressed in LTL, CTL, PSL or as invariants, and verified using BDD or SAT-based algorithms.
Applicable to any control system
The library of elementary function blocks can be customized to any supplier or platform-specific block language. The basis can be IEC 61131-3, but non-standard features like signal validity (common in nuclear applications) are also supported. Block internal logic can be specified in SMV script or as composite diagrams and then checked with NuSMV before use.
