The focus of this paper is on formal modeling and analysis of service-oriented computing (Soc). The contributions of the paper are many: it proposes a specification language, SocL, for specifying service properties; it describes an abstract model called a doubly labeled transition system to define the semantics of SocL; and it introduces a concrete language called COWS for describing the behavior of service agents, along with a method for verifying that a COWS description satisfies properties specified in SocL, and a verification tool, CMC. SocL uses branching time logic with specific primitives for expressing service properties. SocL is interpreted over a doubly labeled transition system whose states and transitions are labeled. COWS is a process algebraic language based on pi-calculus, with specific primitives for expressing service actions. CMC extends SocL with an appropriate standard branching time model-checking algorithm. The whole methodology is evaluated with two detailed case studies.

The paper is well written, with ample intuitive explanations and illustrative examples, which make the reading easier. It is one of the earliest and most extensive works on formal modeling and analysis of service-oriented computing. I recommend this paper for researchers interested in the formal modeling and analysis of service-oriented computing systems.