Monitoring safety properties of composite web services at runtime using CSP

Nowadays, service oriented architecture has been given strong attention as an important approach to integrate heterogeneous systems, in which complex services are created by composing simpler services offered by various systems. The correctness of composition requires techniques to verify if the composite service behaves properly. To this end, in this paper we propose a new method for runtime monitoring of composite services which uses Communicating Sequential Processes (CSP) to specify properties formally. Then, the CSP specification of properties is translated to a Labeled Transition System (LTS). In order to verify the safety of a composite service, we traverse the generated LTS at runtime. Existing methods almost use temporal logic to specify safety properties. There are two advantages in using CSP: 1) similarity of CSP operators and service composition patterns makes CSP straightforward to be used by users. 2) there are some properties which can not be specified by temporal logic, while they can be expressed using CSP.