Title :
Formal Analysis and Verification of a Multimedia Messaging Service Protocol
Author :
Wang, Kemin ; Wang, Yongbin ; Zhou, Shizheng ; Wang, Xiaohong
Author_Institution :
Dept. of Comput., Commun. Univ. of China, Beijing, China
Abstract :
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 UPPAAL´s Editor and simulated its trace by UPPAAL´s Simulator, and checked its safe property using the UPPAAL´s Verifier. And the result reveals the correctness of the system model.
Keywords :
automata theory; electronic messaging; formal verification; telecommunication computing; MMS protocol; NOKIA; UPPAAL; formal analysis; formal verification; model checking; multimedia messaging service protocol; timed automata model; Automata; Message service; Multimedia communication; Protocols; Receivers; System recovery; Transmitters; Formal Analysis; MMS; Model-checking; Timed Automata; UPPAAL; Verification;
Conference_Titel :
Computational Sciences and Optimization (CSO), 2011 Fourth International Joint Conference on
Conference_Location :
Yunnan
Print_ISBN :
978-1-4244-9712-6
Electronic_ISBN :
978-0-7695-4335-2
DOI :
10.1109/CSO.2011.138
