雖然現今化工廠的製程日趨複雜，但其操作步驟仍然是由人工方式制定出來的，這種方式顯然是費時費力且易出錯的。為了確保操作的效率與安全無虞，在本研究中利用自動機模式及動態模擬驗證，將合成、驗證並評估操作步驟的工作系統化，具體來說可以依以下方法進行。
首先，須將系統中所有狀態變數離散化，並根據工程知識，利用非時間自動機對所有一般單元進行建模。再來須利用Aspen Plus Dynamics預做模擬，找出程序單元狀態之間的轉移時間，並據以建構時間自動機模型。接下來再將操作步驟劃分為若干階段後，並設計各階段之控制規範，及建造相應自動機。最後須利用模擬軟體UPPAAL將上述所建之自動機整合，並找出最短或最快之路徑，且將各階段之路徑圖整理並合併成順序功能圖(SFC)。我們利用模擬軟體Aspen Plus Dynamics驗證前述之SFC，若為驗證失敗或希望尋找更多路徑時，須回到控制規範進行增減或修改，再重複上述流程進行合成其餘操作步驟。
根據此一方法我們已成功合成出驟餾罐開車、蒸餾塔開車及反應蒸餾塔啟動之操作步驟，並利用Aspen Plus Dynamics評估其可行性及經濟性。

Despite the fact that the modern chemical plants are becoming much more complex than they used to be, their operating procedures are still generated manually in most cases. Since this approach is clearly laborious, time-consuming and error prone, it is necessary to develop a viable approach to systematically and automatically conjecture a set of reliable control actions to perform various tasks in realistic chemical processes. With timed automata and dynamic simulation, the tasks of synthesizing, validating and evaluating operating procedures have been accomplished in this work. Specifically, the following steps are carried out:
First of all, it is necessary to discretize all state variables in the given system and then build the untimed automata for modeling the basic components according to generic engineering knowledge. Secondly, the elapsed times of all possible state transfers for every processing unit can be determined with Aspen Plus Dynamics and the corresponding timed automata can then be built to model these units. Next, after identifying the critical stages of the entire operation, one can stipulate the control specifications of each stage and build the corresponding automata. All automata built above should then be integrated and synthesized into a system model. Consequently, the shortest or quickest trace in the system may be extracted with UPPAAL and every trace summarized with a sequential function chart (SFC). Finally, the SFCs should be verified with Aspen Plus Dynamics. If the simulation study confirms that all SFCs are unsafe and/or infeasible, one should modify/add/remove the control specifications and repeat the aforementioned synthesis steps.
The above procedure has been applied successfully to three examples, i.e., the start-up operations of a continuous flash drum, a continuous distillation column and a continuous reactive distillation column.

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

Aylett, R., Petley, G., Chung, P., Soutter, J., & Rushton, A. (1997). Planning and chemical plant operating procedure synthesis: a case study. In European Conference on Planning (pp. 39-51). Springer, Berlin, Heidelberg.

Behrmann, G., David, A., & Larsen, K. G. (2004). A tutorial on UPPAAL. In formal methods for the design of real-time systems (pp. 200-236). Springer, Berlin, Heidelberg.

Behrmann, G., David, A., & Larsen, K. G. (2006). A tutorial on Uppaal 4.0. Department of computer science, Aalborg university, Denmark.

Chen, T. Y., & Chang, C. T. (2019). Design approach to synthesize, validate, and evaluate operating procedures based on untimed automata and dynamic simulation. Industrial & Engineering Chemistry Research, 58(19), 8172-8183.

Fusillo, R. H., & Powers, G. J. (1987). A synthesis method for chemical plant operating procedures. Computers & Chemical Engineering, 11(4), 369-382.

Fusillo, R. H., & Powers, G. J. (1988). Operating procedure synthesis using local models and distributed goals. Computers & Chemical Engineering, 12(9-10), 1023-1034.

Kim, J., & Moon, I. (2000). Synthesis of safe operating procedure for multi-purpose batch processes using SMV. Computers & Chemical Engineering, 24(2-7), 385-392.

Kim, J., & Moon, I. (2010). Model checking for automatic verification of control logics in chemical processes. Industrial & Engineering Chemistry Research, 50(2), 905-915.

Lai, J. W., Chou, H. H., & Chang, C. T. (2006). Petri‐net based integer programs for synthesizing optimal material‐transfer procedures in pipeline networks. Journal of the Chinese Institute of Engineers, 29(2), 337-346.

Lakshmanan, R., & Stephanopoulos, G. (1988). Synthesis of operating procedures for complete chemical plants—I. Hierarchical, structured modelling for nonlinear planning. Computers & Chemical Engineering, 12(9-10), 985-1002.

Lakshmanan, R., & Stephanopoulos, G. (1988). Synthesis of operating procedures for complete chemical plants—II. A nonlinear planning methodology. Computers & Chemical Engineering, 12(9-10), 1003-1021.

Lakshmanan, R., & Stephanopoulos, G. (1990). Synthesis of operating procedures for complete chemical plants—III. Planning in the presence of qualitative, mixing constraints. Computers & Chemical Engineering, 14(3), 301-317.

Lee, Y. H., Chang, C. T., Wong, D. S. H., & Jang, S. S. (2011). Petri-net based scheduling strategy for semiconductor manufacturing processes. Chemical Engineering Research and Design, 89(3), 291-300.

Li, J. H., Chang, C. T., & Jiang, D. (2014). Systematic generation of cyclic operating procedures based on timed automata. Chemical Engineering Research and Design, 92(1), 139-155.

Lu, Y. C., Chen, Z. L., & Lee, H. Y. (2017). Optimal start-up strategies for a conventional distillation column using simulated annealing. Chemical Engineering Transactions, 61, 901-906.

O'SHIMA, E. (1978). Safety supervision of valve operations. Journal of Chemical Engineering of Japan, 11(5), 390-395.

Pilavachi, P. A., Schenk, M., Perez-Cisneros, E., & Gani, R. (1997). Modeling and simulation of reactive distillation operations. Industrial & Engineering Chemistry Research, 36(8), 3188-3197.
Scenna, N. J., Ruiz, C. A., & Benz, S. J. (1998). Dynamic simulation of start-up procedures of reactive distillation columns. Computers & Chemical Engineering, 22, S719-S722.

Vaandrager, F. (2011). A first introduction to uppaal. Deliverable no.: D5. 12 Title of Deliverable: Industrial Handbook, 18, Netherlands.

Wang, Y. F., Chou, H. H., & Chang, C. T. (2005). Generation of batch operating procedures for multiple material-transfer tasks with petri nets. Computers & chemical engineering, 29(8), 1822-1836.

Yang, Y. H. A perti-net based optimization strategy for generating the batch operation procedures. Master. Thesis, Cheng Kung University, 2008.

Yeh, M. L., & Chang, C. T. (2012). An automata based method for online synthesis of emergency response procedures in batch processes. Computers & Chemical Engineering, 38, 151-170.

Yeh, M. L., & Chang, C. T. (2012). An automata-based approach to synthesize untimed operating procedures in batch chemical processes. Korean Journal of Chemical Engineering, 29(5), 583-594.