Visual Verifier – a software tool which analyses models of control systems and proves their properties. The tool includes model-checkers capable of verifying properties on the set of reachable states of the system.  The formal verification technique can provide answers to questions like: Will the system behave correctly at all possible combinations of its inputs, including malfunctions of sensors or actuators ? Are all the trajectories of system’s behaviour free from failures ?
	Visual Model Editor that allows creation and modification of model components in modelling language of Net Condition/Event Systems (NCES).  This modelling language is very similar to the IEC 61499 function blocks but has a completely formal semantics.

DOWNLOAD free trial version of the VisualVerifier framework with documentation by clicking on this link. The documentation can be separately downloaded from HERE (PDF, 3Mb)).

RATIONALE of using Formal Verification in Design of Distributed Controls:

Distributed systems are difficult to design. They are also very difficult to debug. Traditional debugging fails even in the case of multi-threaded programs, not speaking about truly decentralized applications executed on several computers.  The IEC 61499 reference architecture provides a unique opportunity of representing the entire distributed systems using one description language. Hence, a complete system can be analysed.

Click here for an overview of the Visual Verification use in industrial automation

The next step, to a mathematically rigorous model can be facilitated using software tools called model-generators. Such a Model Generator has been developed that reads program source code (in IEC 61499) and generates input models for the Visual Verifier.  The Model Generator is a plug in of the FBench – Open Function Block Engineering Tool. Contactinfo@fb61499.com for further details.