| Summary: | 碩士 === 國立交通大學 === 資訊工程系 === 90 === 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.
|
|---|
