Formal verification of sequence controllers

Sequence controllers are widely used in the chemical processing industries due to the inherently sequential nature of many process operations. In part icular, start-up and shut-down operations in continuous processes and any b atch operation require sequence controls to force the time-dependent progre ssion of the operation. One incorrect sequence embedded in a sequence contr ol system can potentially cause severe problems. Therefore, all sequences e mbedded in a sequence control system need to be checked for consistency wit h design specifications. A formal verification methodology is developed tha t can systematically verify the functionality of sequence control systems r epresented at the logic level. Our approach is based on extensions of the r ecently developed implicit model checking technology, which is particularly well suited to the verification of large and complex systems. The sequence control system is represented implicitly as a system of Boolean equations, and the sequences to be verified are specified formally with temporal logi c. Formal verification then requires the solution of a series of Boolean sa tisfiability problems, which are solved efficiently as integer programming feasibility problems. The methodology is applied to a simplified sequence c ontrol system to illustrate its application during the design of sequence c ontrol systems. Finally, the methodology is applied to an existing industri al burner management system. (C) 2000 Elsevier Science Ltd. All rights rese rved.