Wireless protocol testing and validation supported by formal methods. A hands-on report

Bieber, 1996, Formal techniques for an ITSEC-E4 Secure Gateway Bluetooth SIG, 2003. Bluetooth Core Specifications, version 1.1. Available from <www.bluetooth.org> Burguillo-Rial, J.C., Fernández-Iglesias, M.J., González-Castaño, F.J., Llamas-Nistal, M., 2002. Heuristic-driven test case selection from formal specifications. A case study. In: Proceedings of FME 2002. Lecture Notes in Computer Science, vol. 2391, pp. 436–448 Butler, R., Miller, S., Potts, J., Carreño, V.A., 1998. A formal methods approach to the analysis of mode confusion. In: Proceedings of the 17th AIAA/IEEE Digital Avionics Systems Conferefce Cernuda, O., 2003. Vodafone restablece el servicio siete horas después de la averı́a que ha dejado incomunicados a sus clientes (Vodafone resumes normal service seven hours after a failure that kept its clients incommunicated). El Mundo del Siglo XXI/navegante.com (Spanish national newspaper), 20 February Easterbrook, 1997, Formal methods for V&V of partial specifications: an experience report Electronic Guidebook Research Project page, 2003. WWW document <http://www.exploratorium.edu/guidebook> ETSI document TS 122 071 V3.2.0 Fernández-Iglesias, M. J., González-Castaño, F. J., Pousada-Carballo, J. M., Llamas-Nistal, M., Romero-Feijoo, A., 2001. From complex specifications to a working prototype. A protocol engineering case study. In: Proceedings of FME 2001. Lecture Notes in Computer Science, vol. 2021, pp. 57–76 Fleck, 2002, Rememberer: a tool for capturing museum visits, Lecture Notes in Computer Science, 2498, 48, 10.1007/3-540-45809-3_4 González-Castaño, F.J., Garcı́a-Reinoso, J., 2002. Bluetooth Location Networks. In: Proceedings of IEEE Globecom González-Castaño, F.J., Garcı́a-Reinoso, J., 2003. Survibable Bluetooth Location Networks. In: Proceedings of IEEE International Conference on Communications Hao, 2000, Testing ip routing protocols. From probabilistic algorithms to a software tool, 249 Harter, A., Hopper, A., Steggles, P., Ward, A., Webster, P., 1999. The anatomy of a context-aware application. In: Proceedings of the Fifth Annual ACM/IEEE International Conference on Mobile Computing and Networking, pp. 59–68 Haxthausen, 2000, Formal development and verification of a distributed railway control system, IEEE Transactions on Software Engineering, 26, 687, 10.1109/32.879808 Holloway, C.M., 1997. Why engineers should consider formal methods? In: Proceedings of the 16th AIAA/IEEE Digital Avionics Systems Conference, vol. 1, pp. 1.3-16–1.3-22 Holloway, 1996, Impediments to industrial use of formal methods, IEEE Computer, 29, 25 Holzmann, 1994, Proving the value of formal methods Hsi, 2002, The electronic guidebook: a study of user experiences using mobile web content in a museum setting, 48 Holzmann, 1997, The model checker spin, IEEE Transactions on Software Engineering, 23, 279, 10.1109/32.588521 Holzmann, 2003 Jonkers, 1995, OMT*, bridging the gap between analysis and design Kindberg, 2001, A web-based nomadic computing system, Computer Networks, 35, 443, 10.1016/S1389-1286(00)00181-X Leduc, G., Bonaventure, O., Koerner E., Léonard, L., Pecheur, C., Zanetti, D., 1996. Specification and verification of a TTP protocol for the conditional access to services. In: Proceedings of the 12th J. Cartier Workshop on Formal Methods and their Applications Mao, W., Nicol, D.M., 1994. On k-ary n-cubes: theory and applications. CR-194996 ICASE report # 94-88, NASA Nieh, 1994, Modelling and analyzing cryptographic protocols using Petri net, vol. 718, 275 Priyantha, N.B., Chakraborty, A., Balakrishnan, H., 2000. The cricket location-support system. In: Proceedings of the Sixth Annual ACM International Conference on Mobile Computing and Networking Steinert, 2000, Generation of realistic signalling traffic in an ISDN load test system using SDL user models, 219 Tanenbaum, 2003 Umedu, T., Terashima, Y., Yasumoto, K., Nakata, A., Higashino, T., Taniguchi, K., 2002. A Language for describing wireless mobile applications with dynamic establishment of multi-way synchronization channels. In: Proceedings of FME 2002. Lecture Notes in Computer Science, vol. 2391, pp. 607–624 Varshney, 2000, Mobile commerce: A new frontier, Computer, 10, 32, 10.1109/2.876290 Werb, 1998, A positioning system for finding things indoors, IEEE Spectrum, 35, 71, 10.1109/6.715187 Woodruf, A., Aoki, P.M., Hurst, A., Szymanski, M.H., 2001. The guidebook, the friend and the room: visitor experience in a historic house. In: Proceedings of the ACM SIGCHI Conference on Human Factors in Computing Systems, 2001, pp. 273–274 Yamasaki, T., Kishimoto, M., Komoda, N., Oiso, H., 2001. An information offering system for exhibition explanation by Bluetooth technology. In: Proceedings of the SSGRR 2001, Advances in Infrastructure for Electronic Business, Science and Education on the Internet, L'Aquila, Italy, pp. 273–274