在批次製程中的操作步驟大多是以人工的方式執行，但這樣的方式缺乏系統化且容易產生缺失。為了確保實際操作效率與安全，我們在本研究中發展出以時間自動機模式為基礎並且藉由模型驗證工具UPPAAL產生在正常狀態時的周期性操作。具體而言，若要找出在正常狀態時的周期性操作，首先，(1)將系統中所有設備元件的時間自動機模式建構出來，其次(2)將系統中驅動元件的控制規則自動機模式建構出來，再來(3)將前述兩種模型做平行組合後，(4)利用模型驗證工具來驗證系統的正確性並找出最佳操作路徑。最後，(5)將路徑圖整理後可得到操作步驟的順序功能圖與甘特圖。另外，若當系統處在不正常狀態時，為了使系統調整回正常狀態以利後續進行周期性操作，我們額外添加一個校正模型使系統導回至正常起始狀態。在本論文中我們以實際的案例來展現此方法的可行性。

In batch processes, the operation steps mostly are generated manually on an ad-hoc basis, but it is unsystematic and prone to human errors. In order to avoid human errors and to make sure the operational efficiency and safety, it is necessary to develop a feasible approach to generate operation steps in batch processes. In this work, timed automata model coupled with the model-checking tool UPPAAL is carried out to generate cyclic operation steps of normal states in batch processes. Practically, to find the cyclic operation steps of normal states, firstly, (1) timed automata model are constructed for all of the equipments in the corresponding system. Secondly, (2) control rule automata model then is build. In the third step, (3) the aforementioned models are composed in parallel. Forth, (4) a model-checking tool is applied to find the best operational path. As for the last, (5) the resulting operational path is sorted out to get the SFC and Gantt chart. In addition, if the corresponding system is in abnormal condition, an adjustment model can be added in order to make the system returns back into the normal state. In this thesis, practical cases are investigated to show the feasibility of this method.

1.Alur, R., & Dill, D. L. A theory of timed automata. Theoretical Computer Sci. 126, 183-235, 1994.

2.Behrmann, G., David, A., Larsen, K. G. A Tutorial on UPPAAL 4.0. Nov, 2006.

3.Bengtsson, J., Griffioen, W. O., Kristoffersen, K. J., Larsen, K. G., Larsson, F., Pettersson, P., Yi, W. Automated verification of an audio-control protocol using UPPAAL. The Journal of Logic and Algebraic Programming, 163-181, 2002.

4.Cassandras, C. G. & Lafortune, S. Introduction To Discrete Event System. Kluwer Academic. 1999.

5.Clarke, E. M., Emerson, A., Sistla, K. L. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Lang. and Sys. 8, 244-263, 1986.

6.David, A., Illum, J., Larsen, K. G. Model-based Framework for Schedulability Analysis Using UPPAAL4.1. Jan, 2009.

7.Ferrarini, L., Piroddi, L. Modular design and implementation of a logic control system for a batch process. Comput. Chem. Eng., vol. 27, 983-996, 2003.

8.Foulkes, N. R., Walton, M. J., Andow, P. K., and Galluzzo, M. Computer-aided synthesis of complex pump and valve operations. Comput. Chem. Eng., vol. 12, 1035-1044, 1988.

9.Hung, C. L. A Petri-Net Based Approach for On-Line Fault Diagnosis in Batch Process. Master. Thesis, Cheng Kung University, 2007.

10.Katoen, J. P. Concepts, Algorithms and Tools for Model Checking. Lecture Notes of the Course, Mechanised Validation of Parallel Systems, May, 1999.

11.Kim, J., Moon, Il. Automatic verification of control logics in safety instrumented system design for chemical process industry. Journal of Loss Prevention in the Process Industries. 22, 975-980, 2009.

12.Kim, J., Moon, Il. Model Checking for Automatic Verification of Control Logics in Chemical Process. Ind. Eng. Chem. Res, 50, 905-915, 2011.

13.Kristofferson, K. J., Compositional Verification of Concurrent Systems. Ph.D. Thesis, Aalborg University, 1998.

14.Lai, J. W. Petri-Net Based Integer Programs for Synthesizing Optimal Batch Operation Procedures. Master. Thesis, Cheng Kung University, 2006.

15.Li, L. L., Jin, Z., Li, G. Modeling and Verifying Services of Internet of Things Based on Timed Automata. Chinese Journal of Computers, vol. 34, no. 8, 1365-1377, Aug, 2011.

16.Lonn, H., Pettersson, P. Formal verification of a TDMA protocol startup mechanism. Proc. of the Pacific Rim Int. Symp. on Fault-Tolerant Systems, 235-242, Dec, 1997.

17.Moon, Il., Powers, G. J. Automatic Verification of Sequential Control Systems Using Temporal Logic. AIChE Journal, vol. 38, no. 1, 67-75, 1992.

18.O’Shima, E. Safety supervision of valve operation. Journal of Chem. Eng. of Japan, vol. 11, 390-395, 1978.

19.Petterssoon, P. Modelling and Verification of Real-Time Systems. Ph.D. Thesis, Uppsala University, 1999.

20.Rivas, J. R., Rude, D. F. Synthesis of failure-safe operation, AIChE Journal, vol. 20, 320-325, 1974.

21.Uthgenannt, J. A. Path and equipment allocation for multiple, concurrent process on networked process plant units. Comput. Chem. Eng., vol. 20, 1081-1087, 1996.

22.Wang, Y. F. Application of Petri-Net Models for Safety Analysis of Batch Operations. Ph.D. Thesis, Cheng Kung University, 2004.

23.Yang, S. H., Tan, L. S., He, C. H. Automatic verification of safety interlock systems for industrial processes. Journal of Loss Prevention in the Process Industries. 14, 379-386, 2001.

24.Yang, Y. H. A Perti-Net Based Optimization Strategy for Generating the Batch Operation Procedures. Master. Thesis, Cheng Kung University, 2008.

25.Yeh, M. L., Chang, C. T. An Automata-based approach to synthesis untimed operating procedures in batch chemical processes. Korean J. Chem. Eng, vol. 29, no. 5, 583-594, 2012.

26.Yeh, M. L., Chang, C. T. An automata based method for online synthesis of emergency response procedures in batch processes. Comput. & Chem. Eng. 38, 151-170, 2012.

27.Zhao, J., Xu, H., Li, X., Zheng, T., Zheng, G. Partial Order Path Technique for Checking Parallel Timed Automata. Springer-Verlag, 417-432, 2002.