Modeling and Analyzing the WAP Class 2 Wireless Transaction Protocol Using Event-B

Authors: Rajaa Filali, Mohamed Bouhdadi

Abstract:

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.

Keywords: Event-B, wireless transaction protocol, refinement, proof obligation, Rodin, ProB.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1132451

References:

[1] WAP Forum. Wireless Application Protocol Wireless Transaction Protocol Specification. Available via http://www.wapforum.org/, 12 Jul 2001.
[2] S. Gordon and J. Billington, Analysing the WAP class 2 wireless transaction protocol using coloured Petri nets, Springer Berlin Heidelberg, 2000.
[3] Y. T. He, Verification of the WAP transaction layer using the model checker SPIN, 2003.
[4] J. R. Abrial, Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
[5] D. Cansell, and D. Méry, The Event-B Modeling Method: Concepts and Case Studies. Springer, 2007.
[6] R. J. Back, On the correctness of refinement steps in program development, Department of Computer Science, University of Helsinki, 1978.
[7] M. Fitting, First-order logic and automated theorem proving, Springer Science & Business Media, 1996.
[8] R. Filali and M. Bouhdahi, A Mechanically Proved and an Incremental Development of the Session Initiation Protocol INVITE Transaction. Journal of Computer Networks and Communications, 2014.
[9] R. Filali, and M. Bouhdadi. Formal verification of the Lowe modified BAN concrete Andrew Secure RPC protocol. In RFID and Adaptive Wireless Sensor Networks (RAWSN), Third International Workshop. IEEE. pp. 18-22. 2015.
[10] S. Hallerstede, On the purpose of Event-B proof obligations, In: Abstract state machines, B and Z. Springer Berlin Heidelberg, pp. 125-138. 2008.
[11] C. Jones, I. Oliver, A. Romanovsky, and E. Troubitsyna, RODIN (rigorous open development environment for complex systems), University of Newcastle.
[12] O. Ligot, J. Bendisposto, and M. Leuschel. Debugging event-b models using the prob disprover plug-in, Proceedings AFADL 7, 2007.
[13] J. R. Abrial, The B-Book: Assigning Programs to Meanings, Cambridge University Press, 1996.