Model checking has become an industry practice in the Finnish nuclear industry. Recently, VTT has also applied the method in railway industry projects. In practical customer projects, we have found over a hundred design issues. Together with the utility Fortum, we have also developed a graphical front-end for the NuSMV model checker, aimed at user-friendly verification of (nuclear) I&C logics. Our research activities have recently focused on failure tolerance modelling and compositional verification.
Antti Pakonen received the M.Sc. (Tech.) degree in I&C systems from the Helsinki University of Technology, Espoo, Finland, in 2004. He is currently a Senior Scientist and Project Manager with the VTT Technical Research Centre of Finland Ltd., Espoo, Finland, where he has been employed, since 2002. His research interests include I&C software engineering, I&C architecture evaluation, practical application of model checking in industrial applications, and knowledge management.
G. Lilli