Applying formal methods to PCEP: an industrial case study from modeling to test generation.

Hwang Iksoon 1 Mounir Lallali 2, 3 Ana Rosa Cavalli 3, 4, * Dominique Verchere 5
* Auteur correspondant
1 METHODES
SAMOVAR - Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux
2 Lab-STICC_UBO_CACS_MOCS
UBO - Université de Brest, Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
Abstract : This paper presents the experimental results in applying formal methods to an industrial protocol for constraint-based path computation, called Path Computation Element Communication Protocol (PCEP). The experiments include a number of major activities in model-based testing from modeling to test generation. From the PCEP specification defined by IETF (Internet Engineering Task Force), the functionalities of PCEP are divided into two parts: application and protocol. The protocol part of PCEP is then described in the IF (Intermediate Format) language which is based on communicating timed automata. A number of basic requirements are identified from the PCEP specification and then described as properties in IF. Based on these properties, the validation and verification of the formal specification are carried out using the IF toolset. Test cases are generated using an automatic test generation tool, called TestGen-IF, which uses partial state space exploration guided by test purposes. As a result, some errors and ambiguities have been found in the PCEP standard specification.
Type de document :
Article dans une revue
Journal of Software : Testing, Verification and Reliability, 2012, 22 (5), pp.343--361. 〈10.1002/stvr.445〉
Liste complète des métadonnées

http://hal.univ-brest.fr/hal-00706162
Contributeur : Mounir Lallali <>
Soumis le : samedi 9 juin 2012 - 01:18:26
Dernière modification le : mardi 16 janvier 2018 - 15:54:23

Lien texte intégral

Identifiants

Citation

Hwang Iksoon, Mounir Lallali, Ana Rosa Cavalli, Dominique Verchere. Applying formal methods to PCEP: an industrial case study from modeling to test generation.. Journal of Software : Testing, Verification and Reliability, 2012, 22 (5), pp.343--361. 〈10.1002/stvr.445〉. 〈hal-00706162〉

Partager

Métriques

Consultations de la notice

231