應用模型檢查方法偵測電信系統之特徵交互影響問題

Abstract

特徵交互影響是電信系統中常見的問題，是指一服務運作時干擾到其他服務的正常運作。隨著電信系統中的新服務的快速增加，特徵交互影響發生的機會也就愈大，因此加入一新服務時，需要一系統化的方法來偵測是否會發生特徵交互影響問題；由於模型檢查方法具有擁有自動化及驗證效率高等優點，一舨都用模型檢查方法來作偵測。但因電信系統的複雜度高，應用模型檢查方法作特徵交互影響偵測時常遭遇狀態爆炸問題，目前的研究成果都未針對狀態爆炸問題提出解決之道，因此僅能用於小型或局部的特徵交互影響分析。本研究之目的是針對特徵交互影響偵測的狀態爆炸問題提出解決之道。 狀態爆炸問題發生的主因是電腦要儲存電信系統相關使用者運作時所有交互行為所能發生的狀態，要解決狀態爆炸問題的發生只能在偵測分析過程中避免重複行為或不必要狀態的產生；本研究分析電信系統行為後發現以下兩個特性可加以利用： 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.