Formal implementation of procedural controllers for event-driven sequential systems in chemical processes

This paper describes the application of a method to carry out a formally co rrect implementation of a logic controller for an event-driven process syst em. Given a control architecture and the functional specification of each c ontroller module, formal proofs are established and discharged to demonstra te the logical equivalence between the functional specification and the cod e implementation of logic controllers. The methodology is illustrated with an example. (C) 2000 Elsevier Science Ltd. All rights reserved.