Applying formal methods to PCEP: an industrial case study from modeling to test generation. - Université de Bretagne Occidentale Access content directly
Journal Articles Journal of Software Testing, Verification and Reliability Year : 2012

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

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.

Dates and versions

hal-00706162 , version 1 (09-06-2012)

Identifiers

Cite

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⟩
140 View
0 Download

Altmetric

Share

Gmail Mastodon Facebook X LinkedIn More