Fast and comprehensive verification
Model checking is a formal verification method, aiming at a mathematical proof of the model’s correctness. Through exhaustive search, it can reveal design issues in systems already subjected to testing. Since the checked properties can also address unwanted behaviour, it can quickly reveal errors that could lead to unwanted actuations, contradictory commands, or permanently stuck signals.
Our approach
Semantum’s model-checking services target the logic diagrams used in control applications – either vendor-specific PLC programs, or early design phase functional diagrams. We use requirement specification documents, user manuals, or other functional descriptions to specify formal properties for the logics. Symbolic model checkers like NuSMV then check the logics against those properties. The result is either a proof of correctness, or a counterexample trace, revealing a potential design issue.
