WASET
	%0 Journal Article
	%A Rajaa Filali and  Mohamed Bouhdadi
	%D 2017
	%J International Journal of Computer and Information Engineering
	%B World Academy of Science, Engineering and Technology
	%I Open Science Index 130, 2017
	%T Modeling and Analyzing the WAP Class 2 Wireless Transaction Protocol Using Event-B 
	%U https://publications.waset.org/pdf/10008045
	%V 130
	%X This paper presents an incremental formal development of the Wireless Transaction Protocol (WTP) in Event-B. WTP is part of the Wireless Application Protocol (WAP) architectures and provides a reliable request-response service. To model and verify the protocol, we use the formal technique Event-B which provides an accessible and rigorous development method. This interaction between modelling and proving reduces the complexity and helps to eliminate misunderstandings, inconsistencies, and specification gaps. As result, verification of WTP allows us to find some deficiencies in the current specification.

	%P 1144 - 1148