國立臺灣師範大學博碩士論文全文系統

簡易檢索 / 詳目顯示

回結果列表

研究生：	徐志文 Zhi-Wen Hsu
論文名稱：	ArCats局部性模型分析安全性質和活化性質 Compositional Model Checking Safety and Liveness Properties in ARCATS
指導教授：	鄭永斌 Cheng, Yung-Pin
學位類別：	碩士 Master
系所名稱：	資訊工程學系 Department of Computer Science and Information Engineering
論文出版年：	2006
畢業學年度：	94
語文別：	中文
論文頁數：	79
中文關鍵詞：	局部性分析、ARCATS 、安全性質、活化性質、模型驗證
英文關鍵詞：	Compositional Analysis, Safety Property, Liveness Property, Model Checking, ARCATS
論文種類：	學術論文
相關次數：	點閱：301 下載：4
分享至:	分享至facebook 分享至twitter

查詢本校圖書館目錄查詢臺灣博碩士論文知識加值系統勘誤回報

近年來，局部性模型分析在自動化軟體驗證領域中佔有一席角色。局部性模型分析能夠成功的關鍵在於檢驗的系統模型具有良好的階層架構，同時盡量利用最小化的技術減化子系統的內部行為，達到減緩組態爆炸的發生。透過模型架構重構可以解決不良的模型架構，這增強局部性分析的效能。當利用局部性分析檢驗系統性質時，因為保留過多的系統性質到全域系統中，造成子系統無法最小化的結果，這將大幅消減局部性分析在模型驗證中的效能。

在本篇論文中，我們根據ArCats和其在局部性分析中所提供的良好功能，開發出能夠檢測系統安全性質(safety)和活化性質(liveness)的功能，同時並能夠維持局部性分析的減緩狀態爆炸的優勢。在檢驗安全性質時，我們利用一種類似死結狀態的π狀態，讓違反安全性的系統行為能夠被偵測出來。而在檢驗活化性質時我們使用一種特殊的接受轉移（accept transition）來代表系統符合檢驗性質。這兩種在局部性分析中檢測性質，主要參考Cheung[28][29][30]的研究。但是由於ArCats是以CCS為基礎來提供模型架構重構的功能而Cheung的研究採用的是CSP，本篇論文將針對如何利用以CSP為基礎的驗證技術實做到以CCS為基礎的驗證工具中，同時探討與解決所面臨的困難。

In recent years, compositional model checking is known as a promising approach to combat state explosion problem in the automatic verification techniques. However, the success of such technique relies on a good hierarchy in system architectures so that the states in subsystemscan be minimized and hidden to alleviate state explosion problem. ARCATS is a tool designed for compositional analysis. It provides a technique called model architecture refactoring to address systems which do not possess good compositional hierarchies in their as-built architecture.

In the past, ARCATS can detect deadlocks only. In this thesis, we would like to improve ARCATS to allow safety and liveness properties to be verified in a compositional fashion. To check safety properties, a violation of safety properties is caught as a π state in the system behavior. A π state is very similar to a deadlock state. To check liveness properties, a special global transition called accept transition is added to Buchi automata which represents the liveness properties. These approaches have been proposed in Cheung[28][29][30], which is based on CSP, but we need to implement these approaches in to ARCATS, which is based on CCS. There are several issues to be addressed in this implementation. These issues will be discussed in this thesis.

目錄
摘要-----------------------------------------------------------------------------------------------I
ABSTRACT-------------------------------------------------------------------------------------II
致謝---------------------------------------------------------------------------------------------III
目錄---------------------------------------------------------------------------------------------IV
表格目錄--------------------------------------------------------------------------------------VII
圖目錄----------------------------------------------------------------------------------------VIII
第一章 緒論-------------------------------------------------------------------------------------1
1.1 研究動機-----------------------------------------------------------------------------1
1.2 論文架構-----------------------------------------------------------------------------3
第二章 研究背景-------------------------------------------------------------------------------5
2.1 LABELED TRANSITION SYSTEMS(LTS)--------------------------------------------8
2.2 LTS 的轉換語意------------------------------------------------------------------10
2.2.1 限制操作子（Restriction Operator）---------------------------------------10
2.2.2 合成操作子（Composition Operator）-------------------------------------10
2.3 局部性分析 CRA----------------------------------------------------------------13
（COMPOSITIONAL REACHABILITY ANALYSIS ）---------------------------------------13
2.4 列舉狀態空間---------------------------------------------------------------------13
2.4.1 儲存狀態空間------------------------------------------------------------------14
2.4.2 利用Context Constraints執行狀態空間化減-----------------------------14
2.4.3 利用Branch Bisimulation特性等價執行最小化-------------------------16
2.4.3.1 Weak Bisimulation----------------------------------------------------------17
IV
2.4.3.2 Branch Bisimulation--------------------------------------------------------18
2.5 ARCATS VS. 其他模型檢驗工具----------------------------------------------20
第三章 使用ARCATS進行局部性模型驗證-----------------------------------------23
3.1 使用局部性模型驗證安全性質------------------------------------------------24
3.2 使用加強版局部性模型驗證安全性質---------------------------------------25
3.3 安全性質檢驗引擎---------------------------------------------------------------27
3.4 新型態合成引擎------------------------------------------------------------------32
3.4.1 狀態ID的資料結構-----------------------------------------------------------34
3.4.2 產生新的狀態ID--------------------------------------------------------------34
3.4.3 重新對應( Re-Mapping ) 狀態ID------------------------------------------35
3.5 使用ARCATS檢驗GAS-STATION 系統----------------------------------------37
3.5.1 模型化GAS-STATION--------------------------------------------------------------37
3.5.2 使用ARCATS檢驗GAS-STATION-----------------------------------------------40
第四章 使用ARCATS進行局部性模型驗證-----------------------------------------43
4.1 使用加強版局部性分析檢驗活化性質---------------------------------------43
4.2 活化性質檢驗引擎---------------------------------------------------------------45
4.3 使用ARCATS檢驗 RMTP 協定的活化性質---------------------------------47
4.3.1 The Reliable Multicast Transport Protocol (RMTP)-----------------------47
4.3.2 模型化RMTP 和將檢驗的活化性質--------------------------------------48
4.3.3 利用ArCats 檢驗RMTP-----------------------------------------------------52
第五章 使用ARCATS檢驗系統性質實驗結果分析----------------------------------54
5.1 ARCATS和CRA在檢驗安全性質的結果分析------------------------------54
5.2 ARCATS和CRA在檢驗活化性質的結果分析------------------------------57
第六章 結論與未來研究------------------------------------------------------------------59
V
6.1 結論---------------------------------------------------------------------------------59
6.2 未來研究---------------------------------------------------------------------------60
參考文獻---------------------------------------------------------------------------------------62
附錄---------------------------------------------------------------------------------------------67
APPENDIX -A. CCS FILE FORMAT---------------------------------------------------------67
表格目錄
表格 2-1 ARCATS所提供的工具列表-----------------------------------------------------21
表格 3-1 狀態ID資料結構示意圖-------------------------------------------------------34
表格 5-1 比較CRA 和 ARCATS_CRA在檢驗安全性質RIGHT_CHANGE時的差異---------------------------------------------------------------------------------------------55
表格 5-2比較CRA 和 ARCATS_CRA在檢驗安全性質RIGHT_SERVICE時的差異---------------------------------------------------------------------------------------------56
表格 5-3比較CRA 和 ARCATS_CRA同時在檢驗安全性質RIGHT_SERVICE和RIGHT_CHANGE時的差異--------------------------------------------------------------57
表格 5-4 利用ARCATS檢測LIV_REC3過程比較--------------------------------------58
VII
圖目錄
FIGURE 2-1 模型化DB寫入動作的LTS表示圖............................................................9
FIGURE 2-2 MULTI-WAY RENDEZVOUS 的LTS 溝通模式............................................11
FIGURE 2-3 TWO-WAY RENDEZVOUS的LTS溝通模式..................................................12
FIGURE 2-4 (A) 非決定性狀態機 LTS (B) 決定性狀態 LTS....................................15
FIGURE 2-5 P1 和 P2 為可見弱等價(OBSERVATION WEAK EQUIVALENT)（ P1 P2 ）...............................................................................................................................17 w≡
FIGURE 2-6 LTS P的等價對應圖.................................................................................18
FIGURE 2-7 BRANCHING BISIMULATION的定義.........................................................20
FIGURE 3-1 利用BUTTON-UP的方式平行合成GAS-STATION系統.............................24
FIGURE 3-2 表示安全性質的有限狀態機..................................................................25
FIGURE 3-3 安全檢驗引擎架構圖。..........................................................................27
FIGURE 3-4子系統P1,P2,P3和安全性質S1...............................................................28
FIGURE 3-5 (P1||P2)||P3平行合成詳細圖表.............................................................29
FIGURE 3-6 加入安全性質後的平行合成內部圖表..................................................31
FIGURE 3-7 死結錯亂圖..............................................................................................33
FIGURE 3-8 安全行程製作新狀態ID示意圖..............................................................35
FIGURE 3-9 RE-MAPPING示意圖...................................................................................36
FIGURE 3-10 利用TWO-WAY RENDEZVOUS 的方式製作GAS-STATION的五個子系統38
FIGURE 3-11 兩種安全性質LTS圖示.........................................................................39
FIGURE 3-12在LEVEL_1中做RIGHT_CHANGE安全性質檢驗的子系統 COUNTER...40
FIGURE 3-13 GAS-STATION經過最小化後的最終結果...............................................41
FIGURE 3-14 修正過後的 PUMP MODEL.....................................................................41
FIGURE 3-15 GAS-STATION使用正確的PUMP平行合成並最小化後的最終結果......42
FIGURE 4-1 描述活化性質的LTS...............................................................................44
VIII
FIGURE 4-2 ARCATS的活化檢驗引擎架構圖..............................................................46
FIGURE 4-3 RMTP基本架構圖並顯示RECEIVERS分群的方式...................................47
FIGURE 4-4 RMTP局部性分析架構圖並利用階層方式來表示多點傳送的樹狀結構..............................................................................................................................48
FIGURE 4-5 經由RECEIVER、WATCH和CHANNEL所組成的子系統REC_1.................49
FIGURE 4-6經由DESIGNATED_RECEIVER_B、WATCH_B和CHANNEL_B所組成的子系統DR_B...............................................................................................................50
FIGURE 4-7 兩個活化性質LTS...................................................................................51
FIGURE 4-8 利用ARCATS檢驗活化性質LIV_REC3最小化後的模型狀態圖...........52
                                

Alessandro Cimatti , Edmund M. Clarke , Ofer Strichman , Yunshan Zhu . Bounded Model Checking . ACM 2003.
[3] Bharadwaj R. and Heitmeyer C. . Model checking complete requirements specifications using abstraction. Rep. NRL/MR5540-97-7999. Information Technology Division,Naval Research Laboratory, Washington, DC .1997.
[4] C.A.R. Hoare . Communicating Sequential Processes . Prentice-Hall International Series in Computer Science. Pretice-Hall, Inc. , Upper Saddle River, NJ. 1985
[5] Carl A .Sunshine ,editor . Communication Protocol Modeling . Artech House , Dedham , MA , 1981 .
[6] Corbett , James C . Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering , 2(3):161-180 ,March .
[7] E. Allen Emerson. Handbook of theoretical computer science , chapter Temporal and model logic , page 997-1071 . Elsevier Science Publishers B.V.,1990 .
62
[8] Edmund M. Clarke and E. Allen Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Workshop on logic of Programs, volume 131 of Lecture Notes in Computer Science , Yorktown heights, N.Y.,1981
[9] E. M. Clarke , E. A. Emerson , and A. P. Sistla. Automatic verification of finite-state concurrent system using temporal logic. ACM Transactions on Programming Languages and Systems,8(2):244-263,April 1986.
[10] G. J. Holzmann , The model checker SPIN . IEEE Transaction on Software Enginering ,Volume 23 , Issue 5 : 279-295,May 1997 .
[11] G. R. Andrews, Concurrent Programming – Principles and Practice : The Benjamin/Cummings Publishing Company Ltd.,1991.
[12] Gian-Luigi Ferrari , Stefania Gnesi , Isti-C.N.R.Pisa ,Marco Pistore . A model-checking Verification Environment for Mobile Processes. ACM 2003.
[13] Helmbold , D. and Luckham , D . Debugging Ada tasking programs. IEEE Software. 2,2(Mar),47-57 , 1985 .
[14] Hong-Yi Wang master thesis . On-the-fly Bisimulation Minimization in Compositional Analysis. NTNU 2005.
[15] J. C. Lin and S. Paul ,”RMTP : A Reliable Multicast Transport protocol ” ,presented at IEEE INFOCOMM’96 , San Francisco , California , March 1996
63
[16] K.K. Sabnani , Lapone , A. M. ,and M. U. Uyar , 1989 . An algorithmic procedure for checking safety properties of protocols . IEEE Trans. Commun.37,9(Sept.),940-948 . 1989
[17] Larsen. K. and Milner , R. . Verifying a protocol using relativized bisimulation. In proceedings of the 14th International Colloquium on Automata language and Programming. 1987.
[18] Madelaine, E. and Simone, R. de. The FC2 reference Manual . http://www-sop.inria.fr/meije/verification/doc.html ,INRIA.
[19] Malhotra J. Smolka, S. A. Giacalone and Shapir R. A tool for hierarchical design and simulation of concurrent systems . In Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems ,1988 .
[20] Milner, R. Communication and ConCurrency . Prentice Hall 1989 .
[21] N. Francez. Program verification. International Computer Science. Addison-Weflay , 1992 .
[22] Nina Amila , Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan and Kenneth L. McMillan .An Analysis of SAT-based Model Checking Techniques in an Industrial Environment . ACM 2005.
[23] Orna Kupferman and Moshe Y. Vardi . Model Checking of Safety
64
Properties .ACM , 2001 .
[24] R. E. Bryant. Graph-based algorithms for Boolean function manipulations. IEEE Transactions on Computers , 1986 .
[25] Rob J. Van Glabbeek and W.Peter Weijland . Branching time and abstraction in bisimulation semantics ( extended abstract ). In information processing 89 , G Ritter,ed., North-Holland , pp.613-618, 1989 .
[26] Rob J. Van Glabbeek and W.Peter Weijland . Branching time and abstraction in bisimulation semantics . Journal of the ACM 43(3),pp.555-600 ,1996.
[27] Shing Chi Cheung ,and Jeff Kramer . Context Constraints for Compositional Reachability Analysis . ACM 1996.
[28] Shing Chi Cheung ,and Jeff Kramer . Checking Subsystem Safety Properties in Compositional Reachability Analysis . IEEE Proceedings of ICSE-18 ,1996 .
[29] Shing Chi Cheung ,and Jeff Kramer. Checking Safety Property Using Compositional Reachability Analysis . ACM Transaction on Software Engineering and Methodology ,Vol.8,No.1 ,January 1999.
[30] Shing Chi Cheung , Dimitra Giannakopoulou , and Jeff Kramer . Verification of Liveness Properties Using Compositional Reachability Analysis .ACM SIGSOFT 1999
65
[31] Stephan merz . Model Checking: A Tutorial Overview .ACM, 2001
[32] Wei Jen Yeh , Michal Young .Compositional Reachability Analysis Using Process Algebra . ACM 1991.
[33] Yung-Pin Cheng . Towards Scalable Compositional Analysis by Refactoring Design Models. proceedings of the ACM SIGSOFT 2003 Symposium on the Foundations of Software Engineering(FSE2003).
[34] Yung-Pin Cheng . Refactoring Design Models for Inductive Verification . Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis. (ISSTA2002) Rome, Italy, July 22-24, 2002.
[35] Yung-Pin Cheng . The ArCats reference. http://www.ice.ntnu.edu.tw/~ypc/ArCats.htm
[36] Yu-ju Cheng master thesis. Explicit Compositional State-Space Enumeration with Context Constraint & Counter Examples by Hierarchical Tracing . NTNU 2005.

簡易檢索 / 詳目顯示

相關論文