Nowadays, the verification of hybrid system is a popular topic in the formal method community. The presence of both discrete and continuous phenomena in such systems poses an inspiring challenge for our specification and modeling techniques, as well as for analytic capacities. This has led to the development of new, expressive models, such as timed and hybrid automata, and new verification methods, most notably model checking techniques involving a symbolic treatment of real time aspects.
The important examples of hybrid (embedded) systems are process control programs, which involve the digital control of processing plants, e.g. chemical plants. The classes of process controllers that are of considerable practical importance are those that are implemented using Programmable Logic Controllers (PLCs).
To assess the capacity of state of the art formal methods and tools for the analysis of hybrid systems will describe on the design and verification of PLC program in chemical plant. The using of SPIN model checker for both the verification of a process control program for the given plant and the derivation of optimal control schedules.
As the symbolic calculation of real time model checkers can be quite expensive it is interesting to try and exploit the efficiency of establish non real time model checkers like SPIN in those cases where promising work around seem to exist. It handled the relevant real time properties of the PLC controller using a time abstraction technique.