DocumentCode
2346616
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
fYear
2011
fDate
15-19 April 2011
Firstpage
812
Lastpage
815
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/CSO.2011.138
Filename
5957781
Link To Document