Formal Verification of Requirements using SPIN: A Case Study on Web Services
Raman Kazhamiakin, Marco Pistore, Marco Roveri · 2004
In this paper we describe a novel approach for the formal specication 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 denition of the requirements of agent-oriented sys-tems 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 denition 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 aws both in the strategic and in the process models.