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.