Formal Analysis and Verification of a Multimedia Messaging Service Protocol

摘要：

this paper reports about the formal analysis and verification of a Multimedia Messaging Service Protocol (MMS) used by NOKIA in its products. We started with the Timed Automata models of the MMS protocol, and then we performed verifications by model-checking using the UPPAAL. The Timed Automata models of the MMS were modeled with the UPPAALs Editor and simulated its trace by UPPAALs Simulator, and checked its safe property using the UPPAALs Verifier. And the result reveals the correctness of the system model.

关键词： Formal Analysis Verification MMS Modelchecking Tuned Automata UPPAAL

作者: Kemin Wang Yongbin Wang Shizheng Zhou Xiaohong Wang

作者单位: Department of Computer, Communication University of China, Beijing, 100024, China

会议类型: 国际会议

会议名称: The Fourth International Joint Conference on Computational Science and Optimization(第四届计算科学与优化国际大会 CSO 2011)

会议地点: 昆明、丽江

会议语种:英文

页码: 812-815

在线出版日期: 2011-04-15（万方平台首次上网日期，不代表论文的发表时间）