Premium
Applying formal methods to PCEP: an industrial case study from modeling to test generation
Author(s) -
Hwang Iksoon,
Cavalli Ana R.,
Lallali Mounir,
Verchere Dominique
Publication year - 2012
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/stvr.445
Subject(s) - computer science , path (computing) , protocol (science) , formal methods , computer network , programming language , medicine , alternative medicine , pathology
SUMMARY 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. Copyright © 2011 John Wiley & Sons, Ltd.