Probabilistic risk assessment (PRA) is a systematic and comprehensive methodology to assess the risks of complex systems. PRA is an essential part of the safety management in safety-critical industries, such as the nuclear industry, power production, process industry and transportation. PRA provides vital information to evaluate the importance of critical functions, identify weaknesses in technological systems, and optimise and balance design, operation and maintenance. In the nuclear domain, PRA is used to continuously find ways to improve safety, justify plant modifications, optimise annual maintenance revisions and fulfil regulations.
Model checking is an efficient formal method for the verification of hardware and software designs. Based on model checking, VTT offers a service for verifying that automation system software design fulfils stated requirements. The difference to more common verification methods (like testing or simulation) is that all the possible executions of the system model are taken into account. Exhaustive analysis means that hidden design errors can be found in systems that have already undergone verification through conventional means.