Skip to Main content Skip to Navigation
Journal articles

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
* Corresponding author
1 METHODES-SAMOVAR - Méthodes et modèles pour les réseaux
SAMOVAR - Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance, UBO - Université de Brest
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.
Document type :
Journal articles
Complete list of metadatas
Contributor : Mounir Lallali <>
Submitted on : Saturday, June 9, 2012 - 1:18:26 AM
Last modification on : Wednesday, June 24, 2020 - 4:19:29 PM



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⟩



Record views