In this paper we describe a novel approach for the formal specification and verification of distributed processes in a Web service framework. The formal specification is provided at two different levels of abstraction. The strategic level describes the requirements of the Web service domain, in terms of the different actors participating to it, with their goals and needs and with their mutual dependencies and expectations. The process level shows how these requirements are operationalized into communicating processes running on the different Web servers. We exploit Formal Tropos (FT), a language for the formal definition of the requirements of agent-oriented systems which is based on Linear Time Logic, to model the strategic level. We operationalize the process level using Promela, a language designed to describe communicating concurrent processes and amenable to formal verification. We exploit the Spin model checker to perform formal V&V tasks. At the strategic level, requirements are validated against queries formulated by the designer, while at the process level the Promela specifications are verified against the requirements. The implementation of these V&V tasks required the definition of a novel procedure to encode the FT requirements at the strategic level in Promela. The experiments described in the paper show that the approach is effective in revealing possible flaws both in the strategic and in the process models of the Web service domains

Formal Verification of Requirements using Spin: A Case Study on Web Services

Kazhamiakin, Raman;Pistore, Marco;Roveri, Marco
2004

Abstract

In this paper we describe a novel approach for the formal specification and verification of distributed processes in a Web service framework. The formal specification is provided at two different levels of abstraction. The strategic level describes the requirements of the Web service domain, in terms of the different actors participating to it, with their goals and needs and with their mutual dependencies and expectations. The process level shows how these requirements are operationalized into communicating processes running on the different Web servers. We exploit Formal Tropos (FT), a language for the formal definition of the requirements of agent-oriented systems which is based on Linear Time Logic, to model the strategic level. We operationalize the process level using Promela, a language designed to describe communicating concurrent processes and amenable to formal verification. We exploit the Spin model checker to perform formal V&V tasks. At the strategic level, requirements are validated against queries formulated by the designer, while at the process level the Promela specifications are verified against the requirements. The implementation of these V&V tasks required the definition of a novel procedure to encode the FT requirements at the strategic level in Promela. The experiments described in the paper show that the approach is effective in revealing possible flaws both in the strategic and in the process models of the Web service domains
9780769522227
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11582/2543
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact