SAVVY-WS: A methodology for specifying and verifying web service compositions
Contact person
Domenico Bianculli - domenico.bianculli@usi.ch - University of Lugano, Switzerland (USI)
Description
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.
Demo
N/A
Publications
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
Area
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
None
Relationship with Cloud
None