É«É«À²

The title of the thesis: Practical solutions for the model-checking of fault-tolerant instrumentation and control system logics 

Thesis defender: Antti Pakonen
Opponent: Prof. Alexandre Philippot, l’Université de Reims Champagne-Ardenne (URCA), France
Custos: Prof. Valeriy Vyatkin, Aalto University School of Electrical Engineering

Industrial instrumentation and control (I&C) systems are nowadays often software-based, even in applications critical to the society. Traditionally, the verification of I&C system software is based on, e.g., testing, but complete coverage is typically impossible to achieve. It is especially hard to show that some unwanted action cannot occur. 

Model checking is a computer-assisted verification method that can be used to logically prove that a model of the system is correct. VTT has used the method in Finnish nuclear and rail traffic industry projects and found over a hundred design issues. Hidden faults have been detected in designs already subjected to rigorous testing. 

My thesis examines ways of making the work process of I&C logic model checking more user-friendly, accessible, and cost-effective. I have also studied ways of broadening the scope in which I&C design can be analysed. I show how the failure modes of the underlying I&C hardware can be considered when verifying the application logic. I also show how infinite-state modelling and compositional verification can be applied to logics where the more common approach of symbolic, discrete-state model checking falls short. 

The new techniques explored in the thesis, now already in used in VTT’s projects, have already uncovered design issues in logics that were previously thought too complex to check.

Thesis available for public display 10 days prior to the defence at . 

Contact:
antti.pakonen@vtt.fi 
040 129 2785