Sign In


Model checking methodology for critical system verification


VTT is making research on formal model checking methods and their applicability in system verification.

VTT also has capabilities for consulting industry in system verification by e.g. model checking critical logic designs.

Model checking is a computer-aided verification method developed to formally verify the correct functioning of a system design model against its formal specification. Typically, some variant of state machines are used to model the system, while the specifications are formalized with temporal logics.

Model checking tools use efficient algorithms to verify whether all the behaviors of the system model satisfy the system specification. In case the specification is violated, the model checking tools create counter examples desribing executions of the system model that are violating the property.

In several research and customer projects, VTT has found model checking an efficient method for supplementing e.g. safety analyses of instrumentation and control systems in nuclear power plants.