Consistency Checking of Web Service Contracts

M. Emilia Cambronero, Joseph C. Okika, Anders Peter Ravn

Research output: Contribution to journalJournal articleResearchpeer-review


Behavioural properties are analyzed for web service contracts formulated in Business Process Execution Language
(BPEL) and Choreography Description Language (CDL). The key result reported is an automated technique to check consistency between protocol aspects of the contracts. The contracts are abstracted to (timed) automata and from there a simulation is set up, which is checked using automated tools for analyzing networks of finite state processes. Here we use the Concurrency Work Bench. The proposed techniques are illustrated with a case study that include otherwise difficult to analyze fault handlers.
Original languageEnglish
JournalInternational Journal on Advances in Systems and Measurements
Issue number1
Pages (from-to)29-39
Publication statusPublished - 2008



  • web services, model checking

Cite this

Cambronero, M. E., Okika, J. C., & Ravn, A. P. (2008). Consistency Checking of Web Service Contracts. International Journal on Advances in Systems and Measurements, 1(1), 29-39.