臺灣博碩士論文加值系統

對大型或複雜系統而言，其潛在的錯誤規格常嚴重阻礙其系統開發進度，甚或危及系統運作的可靠度，因此系統規格的驗證實為系統需求工程之關鍵。在系統規格驗證方法上，以派區網路推論系統錯誤有其可行性，但仍缺乏規格可能出現之完整推論與驗證。

因此，本研究提出一多階段驗證方法(Multi-Stages Verification Method, MSVM)，針對系統規格之派區網路做更完整的驗證。基於改良後之規格狀態可達樹，本方法可推論出系統存在的拘束性、死結性、可達性、不一致性與時限性等性質。推論過程中，能逐步紀錄其推論結果，並儲存各性質之錯誤與可能原因於資料庫中。此外，本方法之時限性推論除可找出系統規格中所有的封閉迴路外，並可驗證其最大時間限制的合理性，確保系統規格回授資訊的即時性。

在貢獻上，本研究之驗證方法，不但可推論出特定性質之完整錯誤觸發路徑，可依據該路徑推論其肇因，改善目前規格驗證的局部化限制；對於狀態數爆炸的問題，本研究提出「可達樹深度」策略能逐步呈現目前進度中的錯誤，以解決可達樹完整後方能驗證之問題。

The verification of system specifications is a key for requirement engineering. For a large or complex system, its faulty specification delays the system developing schedule and even affects its reliability after developing. Among the verification methods, Petri Nets is popularly applied to transform the specifications for verifying and inferring the feasibility of specifications. But current Petri Nets methods are with few capabilities for verification issues of the faulty specifications including boundedness, deadlock, reachability, inconsistency and time-issue.

In this paper, we divide the five issues into three stages and propose a Petri Nets based Multi-Stages Verification Method (MSVM) with a new reachability-tree algorithm. By the algorithm, we also provide five algorithms to verify the five issues. MSVM can infer the firing sequences, the faulty location, and find out all close-loops to guarantee the feedback information returning within its time limit. Moreover, the proposed reachability-depth policy can solve the problem of state explosion.

中文摘要........................................i
ABSTRACT........................................ii
致謝............................................iii
目錄............................................iv
圖目錄..........................................vi
表目錄..........................................vii
第一章 緒論.....................................1
1.1 研究背景與動機..............................1
1.2 研究目的....................................2
1.3 研究範圍與限制..............................3
1.4 研究架構....................................3
第二章 文獻探討.................................5
2.1 系統規格的轉換..............................5
2.2 派區網路之驗證..............................8
第三章 多階段規格驗證方法與分析.................11
3.1 定義階段性驗證方法..........................11
3.1.1 三階段五項目之驗證方法....................11
3.1.2 三階段五項目之指標........................14
3.2 相關特性探討................................15
3.2.1 初始狀態的影響............................15
3.2.2 可達樹停止點討論..........................16
3.3 各階段之演算法..............................17
3.3.1 Algorithm 1：派區網路特性分析演算法......19
3.3.2 Algorithm 2：ω-tree分析演算法...........26
3.3.3 Algorithm 3：拘束性演算法與死結演算法....28
3.3.4 Algorithm 4：可達性演算法................34
3.3.5 Algorithm 5：不一致性演算法..............36
3.3.6 Algorithm 6：回授時限演算法..............38
3.4 驗證方法之演算法順序........................41
3.4.1 原預定驗證順序............................41
3.4.2 改變驗證順序..............................42
3.5 實現之驗證軟體..............................44
3.5.1 程式關聯介紹..............................44
3.5.1 資料表格關聯介紹..........................47
第四章 案例分析與探討...........................49
4.1 系統架構....................................49
4.2 案例研究與分析..............................52
4.2.1 MES活動派區網路..........................52
4.2.2 機台流程派區網路..........................61
4.2.3 工程鏈簡化模型之派區網路..................66
4.3 結果與討論..................................73
4.3.1 案例分析結果討論..........................73
4.3.2 可達樹之深度問題討論......................74
4.3.3 MSVM之優缺點.............................78
4.3.4 MSVM驗證之例外...........................81
第五章 結論與未來方向...........................83
5.1 結論........................................83
5.2 未來發展方向................................84
參考文獻........................................85

[1]. T. Murata, “Petri Nets: Properties, Analysis and Applications”, Proceedings of the IEEE, vol. 77, no. 4, April 1989.
[2]. M. M. Gao and M. C. Zhou, “Fuzzy Reasoning Petri Nets,” IEEE Transaction on Systems, Man and Cybernetics, vol. 33, no. 3, pp. 314-324, 2003.
[3]. T. Matsumoto, “Reachability Criterion of Live Free Choice Petri Nets”, Proceedings of IEEE Asia Pacific Conference on Circuits and System 96, November 18~21, 1996.
[4]. C. P. Lin and M. D. Jeng, “An Expanded SEMATECH CIM Framework for Heterogeneous Applications Integration”, IEEE Transactions on Systems, Man, and Cybernetics－Part A: Systems and Humans, vol. 36, no. 1, January 2006.
[5]. A. E. Kostin, “Reachability Analysis in T-Invariant-Less Petri Nets”, IEEE Transactions on Automatic Control, vol. 48, no. 6, June 2003.
[6]. L. Gomes, A. Costa and P. Meira, “From Use Cases to Building Monitoring Systems through Petri Nets”, IEEE ISIE 2005, June 20-23, 2005, Dubrovnik, Croatia.
[7]. W. J. Lee and S. D. Cha, “Integration and Analysis of Use Cases Using Modular Petri Nets in Requirements Engineering”, IEEE Transactions on Software Engineering, vol. 24, no. 12, December 1998.
[8]. M. D. Jeng and W. Z. Lu, “Extension of UML and Its Conversion to Petri Nets for Semiconductor Manufacturing Modeling*”, Proceedings of the 2002 IEEE International Conference on Robotics & Automation Washington, DC May 2002.
[9]. Y. Shinkawa, “Inter-Model Consistency in UML Based on CPN Formalism”, IEEE, XIII Asia Pacific Software Engibeering Coference, 2006.
[10]. O. Fengler and W. Fengler, V. Duridanova, “Modeling of Complex Automation Systems Using Colored State Charts”, Proceedings of the 2002 IEEE lntemational Conference on Robotics & Automation Washington, DC May 2002.
[11]. W. G. Schneeweiss, “Tutorial: Petri Nets as a Graphical Description Medium for Many Reliability Scenarios”, IEEE Transactions on Reliability, vol. 50, no. 2, June 2001.
[12]. J. Wang, Y. Deng and G. Xu, “ Reachability Analysis of Real-Time Systems Using Time Petri Nets ”, IEEE Transactions on Systems, Man, and Cybernetics－Part B: Cybernetics, vol. 30, no. 5, October 2000.
[13]. W. M. Zuberek, “Cluster Tools With Camber Revisiting－Modeling Analysis Using Timed Petri Nets”, IEEE Transaction on Semiconductor Manufacturing, vol. 17, no. 3, August 2004.
[14]. F. Y. Wang, Y. Gao and M. C. Zhou, “A Modified Reachability Tree Approach to Analysis of Unbounded Petri Nets”, IEEE Transactions on Systems, Man, and Cybernetics－Part B: Cybernetics , vol. 34, no. 1, February 2004.
[15]. G. Chiola and R. C. Schiaffino, “A Reachability Graph Construction Algorithm Based on Canonical Transition Firing Count Vectors”, IEEE PNPM''01 Aachen, Sept. 11-14, 2001, Reinhard German and Boudewijn Haverkort (eds.), pages 113-122. 2001.
[16]. H. R. Golmakani and J. K. Mills, “Deadlock-Free Scheduling and Control of Flexible Manufacturing Cells Using Automata Theory”, IEEE Transactions on Systems, Man, and Cybernetics－Part A: Systems and Humans, vol. 36, no. 2, March 2006.
[17]. J. H. Yang, J. P. Tsai and C. C. Chen, “Fuzzy Rule Base Systems Verification Using High Level Petri Nets,” IEEE Transaction on Knowledge and Data Engineering, vol. 15, no. 2, pp. 457-473, 2003.
[18]. R. Karp and R. Miller, “Parallel program schemata”, J. Compute. Syst. Sci., vol. 3, no. 4, pp.147-195, May 1969.
[19]. 林明儀，2007，IC工程鏈之階段成熟度分析語評估方法，國立高雄第一科技大學，系統與控制工程研究所碩士論文。
[20]. 李博勛，2007，系統劇本之轉換與驗證，國立高雄第一科技大學，系統與控制工程研究所碩士論文。
[21].“Renew Manual,” http://www.renew.de
[22]. H. E. Eriksson, M. Penker, B. Lyons, and D. Fado，2005，UML2 百寶箱，朱子傑譯，�眳p資訊股份有限公司。
[23]. 洪維恩，2003，Java2 教學手冊，博碩文化有限公司。
[24]. 楊浩青，2006，工廠網路上課講義，國立高雄第一科技大學製造資訊系統實驗室，高雄，台灣。