Specification and verification of context-dependent services

Naseem Ibrahim, Vangalur Alagar, Mubarak Mohammad

Research output: Contribution to journalConference articlepeer-review

5 Scopus citations


Current approaches for the discovery, specification, and provision of services ignore the relationship between the service contract and the conditions in which the service can guarantee its contract. Moreover, they do not use formal methods for specifying services, contracts, and compositions. Without a formal basis it is not possible to justify through formal verification the correctness conditions for service compositions and the satisfaction of contractual obligations in service provisions. We remedy this situation in this paper. We present a formal definition of services with context-dependent contracts. We define a composition theory of services with context-dependent contracts taking into consideration functional, nonfunctional, legal and contextual information. Finally, we present a formal verification approach that transforms the formal specification of service composition into extended timed automata that can be verified using the model checking tool UPPAAL.

Original languageEnglish (US)
Pages (from-to)17-33
Number of pages17
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
StatePublished - Aug 10 2011
Event7th International Workshop on Automated Specification and Verification of Web Systems, WWV 2011 - Reykjavik, Iceland
Duration: Jun 9 2011 → …

All Science Journal Classification (ASJC) codes

  • Software


Dive into the research topics of 'Specification and verification of context-dependent services'. Together they form a unique fingerprint.

Cite this