Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Improvement of a Service Level Negotiation Protocol using Formal Verification

Abstract : The goal of the pervasive connectivity is to enable mobile users to be permanently connected to the Internet. Mobile users are often connected to wireless networks and consuming services that require quality of service guarantees. Accessing services using wireless technologies may make the service delivery vulnerable to security attacks because of the open medium of these technologies. In this context, we need to guarantee both quality of service and security for mobile users communications. In this paper, we present a protocol for service level negotiation which covers both quality of service and security and assigns a profile to each user in order to optimize and automate the dynamic negotiation. To evaluate and test the good functioning of this protocol, we had performed some test scenarios. Since these scenarios can not be exhaustive, this paper will focus on the formal verification of that negotiation protocol. This verification will be performed to check some properties like deadlock, livelock, unspecified reception or dead code. This paper shows implementation details of the verification achieved using the SPIN model checker tool and its PROMELA high level language. It also describes the detected problems and proposes some solutions.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal-univ-bourgogne.archives-ouvertes.fr/hal-00822000
Contributeur : Nader Mbarek <>
Soumis le : lundi 13 mai 2013 - 16:59:04
Dernière modification le : samedi 18 juillet 2020 - 03:13:35

Identifiants

  • HAL Id : hal-00822000, version 1

Citation

Mohamed Aymen Chalouf, Francine Krief, Nader Mbarek, Tayeb Lemlouma. Improvement of a Service Level Negotiation Protocol using Formal Verification. The Eighteenth IEEE symposium on Computers and Communications, Jul 2013, Split, Croatia. ⟨hal-00822000⟩

Partager

Métriques

Consultations de la notice

557