Title :
Verification of the WAP transaction layer
Author :
He, Yu-Tong ; Janicki, Ryszard
Author_Institution :
Dept. of Comput. & Software, McMaster Univ., Hamilton, Ont., Canada
Abstract :
This paper presents a formal approach of formalizing and verifying the Transaction Layer Protocol design in the approved Wireless Application Protocol architecture (WAP Version 2.0). By using the model checker SPIN, we uncover defects in the protocol, which can lead to deadlock and unfaithful refinement of the service definition. A set of desired properties is then verified for the corrected protocol model.
Keywords :
formal verification; program diagnostics; protocols; system recovery; SPIN model checker; WAP transaction layer verification; corrected protocol model; deadlock; formal approach; formal verification; service definition; transaction layer protocol design formalization; transaction layer protocol design verification; unfaithful refinement; wireless application protocol architecture; Automata; Computer architecture; Helium; Information analysis; Open systems; Routing protocols; Safety; Software tools; System recovery; Wireless application protocol;
Conference_Titel :
Software Engineering and Formal Methods, 2004. SEFM 2004. Proceedings of the Second International Conference on
Print_ISBN :
0-7695-2222-X
DOI :
10.1109/SEFM.2004.1347541
