Model checking the reliability of interactive behaviors for mobile computing

作者：Gao Honghao^*; Miao Huaikou; Wang Shuoping; Mei Jia; Liu Yang

来源：Advances in Information Sciences and Service Sciences, 2011, 3(6): 1-12.

DOI：10.4156/aiss.vol3.issue6.1

• Automated verification
• Communication failure
• Computation tree logic
• Critical behavior
• CTL
• Dynamic re-configuration
• Economic loss
• Engineering applications
• High reliability
• Inter-action protocols
• Interaction
• Interactive behavior
• Liveness
• Model checker
• Model-checking techniques
• Prototype system
• Reachability
• Reliability problems
• Reliability properties
• Runtimes
• T S models
• Transition system

The development of mobile computing is dependent on the new methods, techniques and tools to support engineering applications during all the phases of its life cycle. Especially, considering the complexities of interaction protocol, a communication failure can cause high economic losses. The challenge problems to be solved include: 1) guarantee such critical behaviors as communication reliable, and 2) support the dynamic reconfiguration in case some required services may become unavailable when an interaction is executed at runtime phase, both of which belongs to the scope of the reliability problem of interactive behaviors. This paper will perform the automated verification to ensure high reliability of mobile computing using model checking technique. For this purpose, an approach to modeling the interactive behaviors is proposed by using TS model (Transition Systems model, TS model). The reliability properties, including liveness, safety and reachability, are expressed into the temporal logic formulae, namely, CTL (Computation Tree Logic, CTL). Then the reliability verification for our proposed model of interactive behaviors (TS-mc model) is performed in model checker NuSMV. A prototype system is also discussed, and the experimental results show the significant advantage of our method.

• 出版日期2011
• 单位上海大学