CLAVOS - Continuous Lifelong Analysis and Verification of Open Services

The Continuous and Lifelong Analysis and Verification of Open Services (CLAVOS) project aims at consolidating current service-oriented design methodologies and modeling languages in a rigorous software engineering context. The project revolves around the notion of analysis and verification applied continuously during the whole lifecycle of open systems built out of the composition of services. Services represent reusable software components that provide specific functionality to many clients delivering it through standardized network and middleware infrastructure. In this project we see services as the ultimate state of the evolution of software components. The main difference with respect to a traditional component-based approach concerns the open, dynamic, and flexible nature of service-oriented architectures. A deployed component-based application is owned by a single authority, who has full control over the deployed system and its possible evolution. Service-based systems, instead, involve multiple stakeholders. The developers, who compose a system out of existing services, must rely on parts that are owned and managed by other organizations. The overall quality of the composite service largely depends on the quality of its composing services. To guarantee the required quality, it is not sufficient to perform verification of the composite services at design time. Since autonomous services may change independently, it is also necessary to continuously check the quality of the composite service at run time. Indeed, only a lifelong approach to analysis and verification can ensure that the required functional and non-functional properties are delivered by a service-oriented system. The research goals of CLAVOS target the control of the evolution, and the improvement of the quality of today´s service-oriented systems. A key role in CLAVOS is played by a specification language, which should be able to represent multiple views over the architecture of a service composition. These include both functional and non-functional properties of structural and behavioral models. Formal specifications of service compositions enable their lifelong verification. Design-time verification helps to ensure that services fit within a composition model based on their functional and non-functional specifications, described only at the abstract interface level. Verification is also needed at run time, when actual bindings are resolved, to ensure the detection of problems that may arise in the open world and to react accordingly to fulfill the goal of guaranteeing the required quality of service.