Abstract
In this paper, we present the modeling, validation, and verification of an industrial protocol for constraint-based path computation, called PCEP. From the PCEP specification defined by IETF, we divide the functionalities of PCEP into two parts: application and protocol. The protocol part of PCEP is then described in the IF 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 the IF language. Based on these properties, the validation and verification of the formal specification are carried out using the IF toolset. Test cases are generated by using an automatic test generation tool, called TestGen-IF, which uses partial state space exploration guided by test purposes. As a result of the modeling, validation, and verification, some errors and ambiguities are found in the PCEP specification. Also a number of test cases are obtained which will be used for testing implementations.
This work has been supported by the French competitiveness cluster SYSTEM@TIC, through CARRIOCAS project.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Software Engineering Institute/Carnegie Mellon: Capability Maturity Model Integration (CMMISM) for Software Engineering Version 1.1 (2002)
Bozga, M., Fernandez, J.C., Ghirvu, L., Jard, C., Jron, T., Kerbrat, A., Morel, P., Mounier, L.: Verification and test generation for the SSCOP protocol. Journal of Science of Computer Programming 36, 27–52 (2000)
Jia, G., Graf, S.: Verification experiments on the MASCARA protocol. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 123–142. Springer, Heidelberg (2001)
Bozga, M., Graf, S., Mounier, L.: IF-2.0: A validation environment for component-based real-time systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 343–348. Springer, Heidelberg (2002)
Hessel, A., Pettersson, P.: Model-based testing of a WAP gateway: An industrial case-study. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 116–131. Springer, Heidelberg (2007)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer 1, 134–152 (1997)
Audouin, O., Cavalli, A., Chiosi, A., Leclerc, O., Mouton, C., Oksman, J., Pasin, M., Rodrigues, D., Thual, L.: CARRIOCAS project: an experimental high bit rate optical network tailored for computing and data intensive distributed applications. In: Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series (2007)
Vasseur, J.P., Le Roux, J.L.: Path Computation Element (PCE) Communication Protocol, IETF Internet draft, draft-ietf-pce-pcep-19.txt, work in progress (November 2008)
Bozga, M., Graf, S., Ober, I., Ober, I., Sifakis, J.: The IF toolset. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 237–267. Springer, Heidelberg (2004)
Cavalli, A.R., Montes De Oca, E., Mallouli, W., Lallali, M.: Two complementary tools for the formal testing of distributed systems with time constraints. In: Proceedings of the 12th IEEE/ACM International Symposium on Distributed Simulation and Real-Time Applications, Vancouver, Canada, pp. 315–318 (2008)
Postel, J.: Transmission Control Protocol. RFC 793 (Standard), Updated by RFCs 1122, 3168 (1981)
Fernandez, J.C., Garavel, H., Kerbrat, A., Mounier, L., Mateescu, R., Sighireanu, M.: CADP - A protocol validation and verification toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 437–440. Springer, Heidelberg (1996)
Fernandez, J.-C., Jard, C., Jéron, T., Viho, C.: Using on-the-fly verification techniques for the generation of test suites. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 348–359. Springer, Heidelberg (1996)
Cavalli, A.R., Lee, D., Rinderknecht, C., Zaïdi, F.: Hit-or-Jump: An algorithm for embedded testing with applications to in services. In: Proceedings of FORTE XII / PSTV XIX 1999, pp. 41–56. Kluwer, Dordrecht (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 IFIP International Federation for Information Processing
About this paper
Cite this paper
Hwang, I., Lallali, M., Cavalli, A., Verchere, D. (2009). Modeling, Validation, and Verification of PCEP Using the IF Language. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2009 2009. Lecture Notes in Computer Science, vol 5522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02138-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-02138-1_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02137-4
Online ISBN: 978-3-642-02138-1
eBook Packages: Computer ScienceComputer Science (R0)