跳到主要內容

臺灣博碩士論文加值系統

(18.97.14.86) 您好!臺灣時間:2025/02/09 04:12
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

: 
twitterline
研究生:李哲萱
研究生(外文):Jeh-HsuanLi
論文名稱:利用時間自動機模式產生批次製程之操作步驟
論文名稱(外文):Generating Batch Operation Steps Based on Timed Automata
指導教授:張珏庭
指導教授(外文):Chuei-Tin Chang
學位類別:碩士
校院名稱:國立成功大學
系所名稱:化學工程學系碩博士班
學門:工程學門
學類:化學工程學類
論文種類:學術論文
論文出版年:2012
畢業學年度:100
語文別:中文
論文頁數:183
中文關鍵詞:時間自動機模型驗證批次製程
外文關鍵詞:timed automatamodel-checkingbatch process
相關次數:
  • 被引用被引用:0
  • 點閱點閱:204
  • 評分評分:
  • 下載下載:20
  • 收藏至我的研究室書目清單書目收藏:1
在批次製程中的操作步驟大多是以人工的方式執行,但這樣的方式缺乏系統化且容易產生缺失。為了確保實際操作效率與安全,我們在本研究中發展出以時間自動機模式為基礎並且藉由模型驗證工具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.
摘要 I
Abstract II
誌謝 III
目錄 IV
表目錄 VIII
圖目錄 X
第一章 緒論 1
1.1研究動機 1
1.2文獻回顧 1
1.3研究目的 4
1.4章節與組織 4
第二章 時間自動機的模型的架構 5
2.1建構元素 5
2.2時間自動機模型中的基本裝置 6
2.3平行組合(parallel composition) 9
2.4模型驗證(model checking) 13
2.5計算樹邏輯(computation tree logic,CTL) 15
2.6查詢語言(query language) 17
2.6.1狀態公式 18
2.6.2路徑公式 18
2.7時間的性質 21
2.8緊急與待發位置的時間概念 26
第三章 批式製程操作步驟的擬定方法 28
3.1批式製程的分層結構 28
3.2設備元件及控制規則的建模方法 29
3.2.1系統描述 30
3.2.2設備元件模式 31
3.2.3控制規則模式 36
3.3性質驗證 41
3.4操作動作之時間排程 47
3.5不同的正常起始狀態 - 案例二 47
3.6不正常的起始狀態 - 案例三 55
第四章 案例演練 65
4.1公用空氣乾燥製程 65
4.1.1系統描述 65
4.1.2設備元件模式 67
4.1.3控制規則模式 74
4.1.4性質驗證 77
4.1.5操作動作之時間排程 81
4.1.6不同的正常起始狀態 - 案例4.1-2 82
4.1.7不正常的起始狀態 - 案例4.1-3 92
4.2三個儲存槽系統 103
4.2.1 系統描述 103
4.2.2設備元件模式 104
4.2.3控制規則模式 108
4.2.4性質驗證 113
4.2.5操作動作之時間排程 117
4.2.6不同的正常起始狀態 - 案例4.2-2 117
4.2.7不正常的起始狀態 - 案例4.2-3 125
4.3六個儲存槽系統 136
4.3.1系統描述 136
4.3.2設備元件模式 138
4.3.3控制規則模式 143
4.3.4性質驗證 152
4.3.5操作動作之間排程 155
4.3.6不同的正常起始狀態 - 案例4.3-2 155
4.3.7不正常的起始狀態 - 案例4.3-3 164
第五章 結論與展望 178
參考文獻 179
附錄A:軟體介面說明 182


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.

連結至畢業學校之論文網頁點我開啟連結
註: 此連結為研究生畢業學校所提供,不一定有電子全文可供下載,若連結有誤,請點選上方之〝勘誤回報〞功能,我們會盡快修正,謝謝!
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top