跳到主要內容

臺灣博碩士論文加值系統

(54.224.133.198) 您好!臺灣時間:2022/01/29 21:27
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

: 
twitterline
研究生:林沛欣
研究生(外文):Pei-Hsin Lin
論文名稱:應用模型檢查方法偵測電信系統之特徵交互影響問題
論文名稱(外文):Applying Model Checking to Detect Feature Interactions in Telecommunication System
指導教授:鍾乾癸鍾乾癸引用關係
指導教授(外文):Chyan-Goei Chung
學位類別:碩士
校院名稱:國立交通大學
系所名稱:資訊工程系
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:2002
畢業學年度:90
語文別:中文
論文頁數:52
中文關鍵詞:特徵交互影響模型檢查
相關次數:
  • 被引用被引用:1
  • 點閱點閱:263
  • 評分評分:
  • 下載下載:28
  • 收藏至我的研究室書目清單書目收藏:1
特徵交互影響是電信系統中常見的問題,是指一服務運作時干擾到其他服務的正常運作。隨著電信系統中的新服務的快速增加,特徵交互影響發生的機會也就愈大,因此加入一新服務時,需要一系統化的方法來偵測是否會發生特徵交互影響問題;由於模型檢查方法具有擁有自動化及驗證效率高等優點,一舨都用模型檢查方法來作偵測。但因電信系統的複雜度高,應用模型檢查方法作特徵交互影響偵測時常遭遇狀態爆炸問題,目前的研究成果都未針對狀態爆炸問題提出解決之道,因此僅能用於小型或局部的特徵交互影響分析。本研究之目的是針對特徵交互影響偵測的狀態爆炸問題提出解決之道。
狀態爆炸問題發生的主因是電腦要儲存電信系統相關使用者運作時所有交互行為所能發生的狀態,要解決狀態爆炸問題的發生只能在偵測分析過程中避免重複行為或不必要狀態的產生;本研究分析電信系統行為後發現以下兩個特性可加以利用:
1. 系統中存在許多與驗證性質無關之轉移,如果能夠在分析的過程中省略處理這些與驗證性質無關的轉移,則可減少狀態的產生。
2. 使用者的行為間有對稱關係,即這些行為從分析的角度來看是相同的,不需要重複分析,因此若能先偵測對稱關係而避免重複分析特徵交互影響,則可減少甚多狀態的產生。
根據這兩個特性本研究提出利用Partial Order Reduction與Symmetry Reduction這兩個技巧來解決狀態爆炸問題,並將相關的演算法加入模型檢查工具SPIN中,由範例的數據,本研究所提方法並不影響偵測的正確性,且可大幅降低狀態數目,足證本法的有效性。
Feature interaction is a common problem in telecommunication system. Feature interaction occurs when the operation of one service interferes with operations of the other services. As the rapid increment of new services in the system, the probability for feature interactions is getting more. Since telecommunication system is a complicated system, therefore, it needs a systematic and automatic way to detect potential feature interactions.
Model Checking technique is widely applied to detect feature interactions because it has the advantages of automatic verification and high efficiency. The reachability analysis technique is used to general possible states when applying model checking technique to detect feature interaction. However due to the complexity of telecommunication system, it often suffers state explosion problem. Most of current research results do not make efforts to resolve state explosion problem, so their approaches can only be applied to small-scaled system. The purpose of this research tries to propose some technique to avoid the occurrence of state explosion problem when applying model checking to detect feature interactions.
An approach to resolve state explosion is to avoid redundant analysis of similar behaviors and generating unnecessary state during analysis. After investigation the behaviors of telecommunication system, the following two important properties are found:
1.Some transitions, in the system, do not affect the verified property. If these transitions are ignored during analysis, the number of states generated can be reduced.
2.From property verification viewpoint, the behavior of one user is similar to that of another user. In other words, these symmetric behaviors are equivalent to verified property and need not be analyzed redundantly. If symmetry relation can be detected first, then redundant analysis can be avoided. Therefore, the state space can be reduced dramatically.
According the two properties above, Partial Order Reduction technique and Symmetry Reduction technique are proposed to avoid the generation of unnecessary states. The related algorithms are implemented into the model-checker SPIN. From the result of examples, the state space needed during analysis is largely reduced.
摘要 i
Abstract ii
目錄 iv
圖目錄 vi
表格目錄 viii
第一章 緒論 1
第二章 背景與相關研究 3
2.1. 電話系統簡介 3
2.2. 特徵交互影響(Feature Interaction) 簡介 4
2.3. 特徵交互影響的正規定義 6
2.3.1. 正規化方法介紹 6
2.3.2. 電話系統的模型-服務規格 (Service Specification) 7
2.3.3. 特徵的模型-特性 13
2.3.4. 系統模型與特徵交互影響的定義 16
2.4. 偵測特徵交互影響之相關研究 17
2.4.1. 徹底搜尋法為基礎 17
2.4.2. 應用模型檢查方法 18
2.5. 比較與討論 19
第三章 應用模型檢查方法 21
3.1. 模型檢查簡介 21
3.1.1. 系統模型 21
3.1.2. LTL方程式 22
3.1.3. 模型檢查原理 24
3.2. 以模型檢查進行特徵交互影響分析 28
3.2.1. SPIN與Promela簡介 28
3.2.2. 利用SPIN偵測特徵交互影響 29
3.2.3. 狀態爆炸問題(State explosion) 33
第四章 改善系統驗證效率的方法 36
4.1. Partial Order Reduction (POR) 36
4.1.1. Partial Order Reduction 原理 36
4.1.2. SPIN工具加上POR技巧 42
4.1.3. 驗證結果 42
4.2. 利用Symmetry Reduction 技巧 43
4.2.1. Symmetry Reduction原理 43
4.2.2. SPIN工具加上Symmetry Reduction技巧 46
4.2.3. 驗證結果 47
4.3. 討論 48
第五章 結論 50
參考文獻 52
[1] M.Ben-Ari, Z.Manna, and A. Pnueli. “The temporal logic of branching time.” Acta information, 20:207-226, 1983
[2] M.A. Ardis, Formal Methods for telecommunications system requirements: A survey of standardized languages, Annals of Software Engineering 3, 157-187, 1997
[3] André Arnold, Finite Transition Systems: Semantics of Communicating Systems, Englewood Cliffs, NJ: Prentice Hall, 1994Paris: Masson, 1994
[4] Au, P.K. and Atlee, J.M., “Evaluation of a state-based model feature interactions," Proc. of Fourth Workshop on Feature Interactions in Telecommunications Systems, pp.153-167, July, 1997.
[5] Bowen, T.F., et al., "The feature interaction problem in telecomunication systems," Proc. 7th Int''l. Conf. on Software Eng. for Telecommun. Switching Sys., pp.59-62,July 1989.
[6] M. Calder and E. Magil, Editors, Feature Inteaction in Telecommunications and Software Systems VI, Amsterdam: IOS Press, May 2000
[7] M Calder, E. Magill, M. Kolberg, and S. Reiff-Marganiec., Feature Interaction: A Critical Review and Considered Forecast, Submitted for publication. 2001.
[8] M. Calder and A. Miller, “Using SPIN for feature interaction analysis -a case study”, Proceedings Spin 2001, Lecture Notes in Computer Science, 2057:143 —162, 2001.
[9] Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith, Progress on the State Explosion Problem in Model Checking, Informatics: 10 Years Back, 10 Years Ahead, Reinhard Wilhelm (Ed.), LNCS 2000, Berlin ; Heidelberg ; NewYork ; Barcelona ; Hong Kong ; London ; Milan ; Paris ; Singapore ; Tokyo : Springer, 2001, pp176
[10] E. M. Clarke, E. A. Emerson.“Design and synthesis of synchronization skeletons using branching time temporal logic,” In Proc. Workshop on Logic of Programs (Yorktown Heights, N.Y.), Lecture Notes in Computer Science, 131, Springer Verlag, New York, 1981.
[ 11] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking, Cambridge,MA: MIT Press, pp. 220 - 221, 1999
[12] Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas, A Tutorial Introduction to PVS, Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995
[13] Jan Ellsberger & Dieter Hogrefe & Amardeo Sarma, SDL: Formal Object-oriented Language for Communicating Systems, London: Prentice Hall 1997
[14] E. Allen Emerson,"Temporal and Modal Logic", In Handbook of theoretical computer science, Elsevier Science Publishers B.V.,1990, p.997-1067
[15] E.A. Emerson, S. Jha, D. Peled, Combining partial order and symmetry reductions, in Ed Brinksma (ed.), Proc. of TACAS''97 (Tools and Algorithms for the Construction and Analysis of Systems), LNCS 1217, 19-34, Springer, 1997.
[16] R. Gerth, D. Peled, M. Y. Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of liner temporal logic. In Protocol Specification Testing and Verification,pp. 3-18 Chapman & Hall, 1995
[17] Patrice Godefroid, Partial-Order Methods for Verification of Concurrent Systems: An Approach to the State Explosion Problem, Lecture Notes in Computer Science 1032, Berlin/Heidelberg: Springer-Verlag, 1996
[18] Gerard J. Holzmann, “Design and validation of protocols: a tutorial”, Computer Networks and ISDN Systems, 25:981-1017, 1993.
[19] Gerard J. Holzmann, “The model checker Spin”. IEEE Transactions on Software Engineering, 23(5):279-295, May 1997.
[20] A. Khoumsi, ”Detection and Resolution of Interactions Between Services of Telephone Networks”, Interactions in Telecommunications Systems IV, P. Dini, R. Boutaba, and L. Logrippo, eds., pp. 78—92, IOS Press, 1997.
[21] M. Kolberg, E.H. Magill, D. Marples, and S. Reiff, ”Second FeatureInteraction Detection Contest”, Feature Interactions in Telecommu-nications and Software Systems VI, pp. 293—310, IOS Press, 2000.
[22] Zohar Manna and Amir Pnueli, Temporal Verification of Reactive Systems: Safety, Berlin/Heidelberg: Springer-Verlag, 1995A
[23] K.L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, 1993.
[24] Robin Milner, Communication and Concurrency, New York: Prentice-Hall, 1989
[25] G. Naser, “A Flexible Framework for Detection of FeatureInteractions in Telecommunication Systems”, Lincentiate Dissertation, Department of Computer Systems Infomation Techinology, Uppsala University, 2000
[26] Masahide Nakamura, “Design and Evaluation of Efficient Algorithms for Feature Interaction Detection in Telecommunication Services”, Doctor Dissertation, Engineering Science of Osaka University, 1999
[27] D. Peled and T.Wilke. “Stutter-invarinat temporal properties are expressible without nexttime operator”. Information Processing Letters, 1997
[28] M. Plath, and M. Ryan, ”Plug-and-play features”, Feature Interactions in Telecommunications and Software Systems V, K. Kimbler and L.G. Bouma, eds., pp. 150—151, IOS Press, 1998.
[29] A. Pnueli. ”A temporal logic of concurrent programs.” Theoretical Computer Science, 13:45-60, 1981.
[30] A. Prasad Sistla and E. A. Emerson, Symmetry and Modelchecking, the journal Formal Methods in System Design, Vol. 9, No. 1/2, pp105-131, August 1996
[31] Antti Valmari, “The State Explosion Problem,” in Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science 1491, Springer-Verlag, Berlin/Heidelberg, 1998, pp. 429-528.
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top