From architecture down to implementation of safe process control applications-the lift case study

The paper reports the results of specifying, designing, verifying and implementing safe object oriented process control applications. This work gives a solution which enables the synthesis of a general method for addressing problems associated with these procedures. This method has been applied on several case studies by using the SPIN verification tool. An implementation of the lift controller and a graphical simulation have then been realised using Synchronous C++, a concurrent extension of C++ designed by our team and which is being integrated into Gnu gcc. Liveness and safety properties have been checked on the model to ensure that the system behaviour is correct. This application shows the efficiency of using formal methods in building safe process control applications. It also shows that Synchronous C++ is appropriate for developing process control problems and is easily translatable from synchronous models such as Promela