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 SocL, a logic specifically designed to capture peculiar aspects of services. Service behaviours are abstracted in terms of Doubly Labelled Transition Systems, which 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. Fundamental Approaches to Software Engineering, 11th International Conference, FASE 2008.
A model checking approach for verifying COWS specifications / A. Fantechi; S. Gnesi; A. Lapadula; F. Mazzanti; R. Pugliese; F. Tiezzi. - STAMPA. - (2008), pp. 230-245. [10.1007/978-3-540-78743-3_17]
A model checking approach for verifying COWS specifications
FANTECHI, ALESSANDRO;PUGLIESE, ROSARIO;F. Tiezzi
2008
Abstract
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 SocL, a logic specifically designed to capture peculiar aspects of services. Service behaviours are abstracted in terms of Doubly Labelled Transition Systems, which 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. Fundamental Approaches to Software Engineering, 11th International Conference, FASE 2008.
| File | Dimensione | Formato | |
|---|---|---|---|
|
cows_fase08-springer.pdf
accesso aperto
Tipologia:
Versione finale referata (Postprint, Accepted manuscript)
Licenza:
Open Access
Dimensione
362.85 kB
Formato
Adobe PDF
|
362.85 kB | Adobe PDF |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
