Formal verification of requirements using SPIN: a case study on Web services

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 model the strategic level exploiting Formal Tropos (FT), a language for the formal definition of the requirements of agent-oriented systems which is based on linear time logic. We model 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 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 requires the definition of a novel procedure to encode the FT requirements 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.