Get in contact for a list of our model checking references!

Examples of cases where VTT has applied model checking:

  • Emergency cooling system. The system takes care of reactor cooling if normal cooling systems are unavailable. Model checking was used to analyze the control logic of the system.


  • Arc protection system. The system protects hardware and equipment from electric arcs. Model checking was used to verify triggering logics of the system.


  • Stepwise shutdown system. In case of disturbances in the process, the stepwise shutdown system steers the process into a safe state in a stepwise manner. Control logic and tolerance for single failures were analysed with model checking.


  • Automated changeover switching unit for a busbar. The system switches the power feed to an alternative power supply in case of voltage breaks. The performance of the switching units and the malfunction protection relays were analysed with model checking.


  • Emergency diesel system. The emergency diesels provide reserve power for a critical system. Model checking was used to analyse the control and start up logics of the diesels. In addition, a compositional model checking approach was develop to support verification of large design.


  • Critical function block designs. Several function block designs have been exhaustively verified by model checking in our projects.