A model checking approach for verifying COWS specifications

Alessandro Fantechi, Stefania Gnesi, Alessandro Lapadula, Franco Mazzanti, Rosario Pugliese and Francesco Tiezzi

Dipartimento di Sistemi e Informatica, Universita' di Firenze

We introduce a logical verification framework for checking functional properties of service-oriented applications formally specified using the service specification language COWS. The properties are described by means of a service-oriented logic, called SocL, that is a specialization of the logic UCTL to capture peculiar aspects of services. Service behaviours are abstracted in terms of Doubly Labelled Transition Systems that describe all their possible evolutions and are used as the interpretation domain for SocL formulae. We also illustrate the SocL model checker at work on a bank service scenario specified in COWS.