Synthesis of safe operating procedure for multi-purpose batch processes using SMV

Symbolic model verifier (SMV), an automatic error finding system, is develo ped and applied to various chemical processing systems to test their safety and feasibility. In this paper, we adopted SMV to synthesize error-free op erating schedules in multi-purpose batch processes. The strength of this me thod is to synthesize a feasible sequence and to verify its safety simultan eously. Here, we propose two algorithms. One is to find embedded errors in operating sequences such as violating intermediate storage tank policies an d unavailability due to sudden operating condition changes or insufficient production recipes. The other is the completion time algorithm to make sure that a makespan and a final operating sequence are obtained without errors . The proposed algorithm identifies errors and finds a minimum makespan and an operating sequence. Computation tree logic (CTL) embedded in SMV is ext ensively used to describe the situation of unsafe conditions and time relat ed conditions for the final makespan. As a result of applying the algorithm s to multi-purpose chemical processes, this approach finds a makespan and e rror-free operating schedules successfully. This combined synthesis and ver ification method also reduces the computation time and verifies operating s chedules efficiently compared with the previously published algorithms. (C) 2000 Elsevier Science Ltd. All rights reserved.