Error-free scheduling for batch processes using symbolic model verifier

This paper focuses on the development of a new approach for the synthesis of error-free operating schedules in batch processes. The synthesis of error-free operating procedures for batch processes becomes an important issue in the safe operation of industrial plant. It spends considerable amount of time and effort in scheduling and verifying operating procedures for correctness and completeness. In this study, we adopted SMV (Symbolic Model Verifier), an automatic error finding system, which is applied to various batch processes to test their safety and feasibility. The strength of this method is to minimize safety hazard and operability errors, and adjust process and recipe changes during the planning of operating procedure. The proposed approach identifies embedded errors and finds a minimum makespan and synthesizes an error-free operating sequence at the same time. Several examples are presented to illustrate the effectiveness of the proposed approaches.