Personal tools
You are here: Home Results S-Cube Shopping List for Industry Results SAVVY-WS: A methodology for specifying and verifying web service compositions

SAVVY-WS: A methodology for specifying and verifying web service compositions

by Pierluigi Plebani last modified Jan 11, 2012 10:18

Contact person

Domenico Bianculli - - University of Lugano, Switzerland (USI)




SAVVY-WS aims at providing an integrated approach to support lifelong verification of service compositions. It is based on a specification language, around which design-time and run-time quality assurance activities can be performed. The specification language, based on metric first-order temporal logic, has been designed to express the most common property specification patterns occurring in functional and non-functional requirements of service compositions.  The language specifies the required properties in terms of logical formulae, called assumed assertions  (AAs). Based on the AAs of all services invoked by the workflow, in turn, the composition may offer a service whose properties can also be specified as formulae, called guaranteed assertions (GAs).  At design time a formal verification tool is used to check that a composite service delivers its expected functionality and meets the required quality of service (both specified as GAs), under the assumption that the external services used in the composition fulfill their required interfaces (specified as AAs).  Since in service-oriented systems the traditional boundary between design time and run time is blurring, verification,  must extend to run time. SAVVY-WS supports continuous verification by transforming specifications into run-time assertions. These assertions are used to check for possible deviations from the correct behavior verified at design time.


Technical Information

The specification language is technology independent and can be used to specify workflow-based services. The design-time verification technique requires service implementations to be translatable to a state-transitions system. The run-time verification checker can be integrated within a run-time monitoring architecture.




Luciano Baresi, Domenico Bianculli, Sam Guinea, and Paola Spoletini. Keep it small, keep it real: Efficient run-time verification of web service compositions. In Proceedings of IFIP international conference on Formal Techniques for Distributed Systems (FMOODS/FORTE 2009), Lisbon Portugal, volume 5522 of Lecture Notes in Computer Science, pages 26-40. Springer, June 2009. pdf

Domenico Bianculli, Carlo Ghezzi, Paola Spoletini, Luciano Baresi, and Sam Guinea. A guided tour through SAVVY-WS: a methodology for specifying and validating web service compositions. In Egon Börger and Antonio Cisternino, editors, Advances in Software Engineering, volume 5316 of Lecture Notes in Computer Science, pages 131-160. Springer, November 2008. pdf 



Quality Assurance, Service-oriented Software Engineering


Maturity Level

  • Verification ar design time: Mock-up (new prototype will be built in Q1 2012)
  • Verification at run time: Prototype (single scenario)

Relationship with Future Internet and Internet of Services



Relationship with Cloud


Web site

Document Actions
  • Send this
  • Print this
  • Bookmarks

The Plone® CMS — Open Source Content Management System is © 2000-2017 by the Plone Foundation et al.