Rigorous Software Engineering for Service-Oriented Systems

Service-Oriented Computing is a paradigm where services are understood as autonomous, platform-independent computational entities that can be described, published, categorized, discovered, and dynamically assembled for developing massively distributed, interoperable, evolvable systems and applications. These characteristics have pushed service-oriented computing towards nowadays widespread success, demonstrated by the fact that many large companies invested a lot of efforts and resources to promote service delivery on a variety of computing platforms, mostly through the Internet in the form of Web services. In the past, service-oriented computing and development has been done in a pragmatic, mostly ad-hoc way. Theoretical foundations were missing that are needed for trusted interoperability, predictable compositionality, and quality issues like security, correctness, or resource usage. The IST-FET integrated project

Sensoria

has addressed these issues by developing a novel comprehensive approach to the engineering of service-oriented software systems where foundational theories, techniques and methods are fully integrated in a pragmatic software engineering approach, supporting semi-automatic development and deployment of self-adaptable (composite) services.

Sensoria

is an IST project funded by the EU as Integrated Project (IP) in the 6th Framework Programme (FP6) as part of the Global Computing Initiative (GC). It started on September 2005 and ended on February 2010.

Project

Sensoria

has developed a novel comprehensive approach to deal with Service-Oriented Computing (SOC), where foundational theories, techniques and methods are fully integrated in a pragmatic tool-supported software engineering approach.

The foundational research carried out in

Sensoria

has been steered by a number of case studies for ensuring applicability of

Sensoria

methods and meeting expectations of society and the economy. In this chapter, we introduce these case studies. Three of the case studies came from industrial applications in automotive, finance and telecommunication domains; one came from an academic application for distributed e-learning and course management. Having in mind the relevance that these areas have in society and the economy, the above case studies have been extensively used in

Sensoria

during the whole project.

A trend in software engineering is towards model-driven development. Models are used to document requirements, design results, and analysis in early phases of the development process. However, the aim of modeling is very often more ambitious as models are used for automatic generation in so-called model-driven engineering approaches. The relevance of models leads to the need of both, high-level domain specific modeling languages (DSML), and metamodels which are the basis for the definition of model transformations and code generation.

For the service-oriented computing domain we developed within the

Sensoria

project a DSML for building and transforming SOA models. This DSML is defined as a family of UML profiles, which complement the SoaML profile for the specification of SOAs structure. Our family of profiles focus on orchestration of services, service-level agreements, non-functional properties of services, implementation of service modes and service deployment.

This chapter provides an overview of SRML — the

Sensoria

Reference Modelling Language. Our focus will be on the language primitives that SRML offers for modelling business services and activities, the methodological approach that SRML supports, and the mathematical semantics the underpins the modelling approach, including techniques for qualitative and quantitative analysis.

Businesses typically structure their activities with workflows, which are often implemented in a rather static fashion in their IT systems. Nowadays, system requirements change rapidly as businesses try to maintain their competitive edge, calling for similar agility of the IT systems. To this end, we present

StPowla

, an approach that marries service oriented architecture, policies and workflows to support the agile execution of business workflows. In

StPowla

, the business is modelled by workflows, whose tasks are eventually carried out by services. Adapatation is obtained by allowing the stakeholders to define policies that establish the quality levels required of the services. The prototype

StPowla

support architecture comprizes the transformation of the workflow model into executable WS–BPEL to be deployed in the ODE–BPEL execution engine, the generation of default policies from the model, and the enactment of the policies by the

Appel

policy server. The SENSORIA Finance Case Study is used throughout the paper.

Architectural Design Rewriting

(ADR) is an approach for the design of software architectures developed within

Sensoria

by reconciling graph transformation and process calculi techniques. The key feature that makes ADR a suitable and expressive framework is the algebraic handling of structured graphs, which improves the support for specification, analysis and verification of service-oriented architectures and applications. We show how ADR is used as a formal ground for high-level modelling languages and approaches developed within

Sensoria

.

Core calculi have been adopted in the

Sensoria

project with three main aims. First of all, they have been used to clarify and formally define the basic concepts that characterize the

Sensoria

approach to the modeling of service-oriented applications. In second place, they are formal models on which the

Sensoria

analysis techniques have been developed. Finally, they have been used to drive the implementation of the prototypes of the

Sensoria

languages for programming actual service-based systems. This chapter reports about the

Sensoria

core calculi presenting their syntax and intuitive semantics, and describing their main features by means of a common running example, namely a Credit Request scenario taken from the

Sensoria

Finance case study.

This chapter presents the behavioral theory of some of the

Sensoria

core calculi. We consider

SSCC

,

μ

se

and CC as representatives of the session-based approach and COWS as representative of the correlation-based one.

For

SSCC

,

μ

se

and CC the main point is the structure that the session/conversation mechanism creates in programs. We show how the differences between binary sessions, multiparty sessions and dynamic conversations are captured by different behavioral laws. We also exploit those laws for proving the correctness of program transformations.

For COWS the main point is that communication is prioritized (the best matching input captures the output), and this has a strong influence on the behavioral theory of COWS. In particular, we show that communication in COWS is neither purely synchronous nor purely asynchronous.

In the

Sensoria

project, core calculi have been adopted as a linguistic means to model and analyze service-oriented applications. The present chapter reports about the static analysis techniques developed for the

Sensoria

session-oriented core calculi

CaSPiS

and

CC

. In particular, it presents a type system for client progress and control flow analysis in

CaSPiS

and type systems for conversation fidelity and progress in

CC

. The chapter gives an overview of the these techniques, summarizes the main results and presents the analysis of a common example taken from the

Sensoria

financial case-study: the credit request scenario.

We present a framework for designing and composing services in a “call-by-contract” fashion, i.e. according to their behavior. We discuss how to correctly plan service compositions in some relevant classes of services and behavioral properties. To this aim, we propose both a core functional calculus for services, and a graphical design language. The core calculus features primitives for selecting and invoking services that respect given behavioral requirements, typically safety properties on the service execution history. A type and effect system over-approximates the actual run-time behavior of services. A further static analysis step finds the viable plans that drive the selection of those services matching the behavioral requirements on demand.

We overview the cc-pi calculus, a model for specifying QoS negotiations in service composition that also allows to study mechanisms for resource allocation and for joining different QoS parameters. Our language combines a synchronous channel-based communication mechanism with a set of primitives for constraint handling. We also illustrated a variant of the calculus in which the standard non-deterministic choice is replaced by a prioritised guarded choice that follows a static form of priority favouring its left over its right argument. We show how both versions of the calculus work by considering two case studies of the

Sensoria

Project taken from the Telecommunication and Finance domains. Specifically, we apply the original cc-pi calculus for specifying Telco QoS policies and for enforcing them at execution time, and we formalise in the prioritised cc-pi a QoS-aware negotiation of a credit request service.

One of the ultimate goals of Service Oriented Computing (SOC) is to provide support for the automatic on-demand discovery of basic functionalities that, once combined, correctly compute a user defined task. To this aim, it is necessary for services to come equipped with a computer-understandable interface that allow applications to match the provided functionalities with the user needs. In this context, a prominent issue concerns the compliance between the operations invoked by the client – the client protocol – and the operations executed by the service – the service protocol. Process calculi, the theoretical tools investigated in the Work Package 2 of

Sensoria

, can contribute to the solution of this problem. The idea we present in this chapter is to describe the externally observable message-passing behaviour of services as process calculi expressions; following recently adopted terminology, we call this description the

service contract

. We show how, in certain cases, service contracts can be automatically extracted out of service behaviour, and how they can be used to formally check the compliance among the communication protocols of interacting services.

Languages and models for service-oriented applications usually include primitives and constructs for

exception

and

compensation

handling. Exception handling is used to react to unexpected events while compensation handling is used to undo previously completed activities. In this chapter we investigate the impact of exception and compensation handling in message-based process calculi and the related theories developed within

Sensoria

.

The management of Long Running Transactions is a crucial aspect in the field of Service Oriented Architectures. This chapter reports on the usage of the ESC middleware in the design and implementation of long running transactions. The middleware has been formally defined as a process calculus and supports a model-driven methodology which clearly separates the development stages of long running transactions.

We present our approach to the denotation and representation of hierarchical graphs: a suitable algebra of hierarchical graphs and two domains of interpretations. Each domain of interpretation focuses on a particular perspective of the graph hierarchy: the top view (nested boxes) is based on a notion of embedded graphs while the side view (tree hierarchy) is based on gs-graphs. Our algebra can be understood as a high-level language for describing such graphical models, which are well suited for defining graphical representations of service-oriented systems where nesting (e.g. sessions, transactions, locations) and linking (e.g. shared channels, resources, names) are key aspects.

We show an approach,

CaPiTo

, to model service-oriented applications using process algebras such that, on the one hand, we can achieve a certain level of abstraction without being overwhelmed by the underlying implementation details and, on the other hand, we respect the concrete industrial standards used for implementing the service-oriented applications. By doing so, we will be able to not only reason about applications at different levels of abstractions, but also to build a bridge between the views of researchers on formal methods and developers in industry. We apply our approach to the financial case study taken from Chapter 0-3. Finally, we develop a static analysis to analyse the security properties as they emerge at the level of concrete industrial protocols.

In this chapter we present (some of) the design principles which have inspired the development of the CMC/UMC verification framework. The first of these is the need of an abstraction mechanism which allows to observe a model in terms of an abstract

L

2

TS

, therefore hiding all the unnecessary underlying details of the concrete computational model, while revealing only the details which might be important to understand the system behavior. The second of these is the need a Service-Oriented Logic (

SocL

) which is an event and state based, branching-time, efficiently verifiable, parametric temporal logic, for the formal encoding of service-oriented properties. The third principle is the usefulness of an on-the-fly, bounded model-checking approach for an efficient, interactive analysis of service-oriented systems which starts from the early stages of the incremental system design.

This chapter presents different tools that have been developed inside the

Sensoria

project.

Sensoria

studied qualitative analysis techniques for verifying properties of service implementations with respect to their formal specifications. The tools presented in this chapter have been developed to carry out the analysis in an automated, or semi-automated, way.

We present four different tools, all developed during the

Sensoria

project, exploiting new techniques and calculi from the

Sensoria

project itself.

A Service-Oriented Computing (SoC) architecture consists of a number of collaborating services to achieve one or more goals. Traditionally, the focus of developing services (as software components) has been on the static binding of these services within a single context and constrained in an individual manner. However, service architectures should be dynamic, where service binding and context changes with environmental changes. The task of designing and analysing such architectures becomes very complex. In this chapter we discuss a specification profile and analysis framework for service modes. A service mode provides an encapsulation of both specification and adaptation in different service scenarios. The approach is implemented as a tool suite and integrated into the Eclipse IDE.

The Temporal

Mo

bile

S

tochastic

L

ogic (MoSL) has been introduced in previous works by the authors for formulating properties of systems specified in

StoKlaim

, a Markovian extension of

Klaim

. The main purpose of MoSL is addressing key functional aspects of network aware programming such as distribution awareness, mobility and security and to guarantee their integration with performance and dependability guarantees. In this paper we present SoSL, a variant of MoSL, designed for dealing with specific features of Service-Oriented Computing (SOC). We also show how SoSL formulae can be model-checked against systems descriptions expressed with

MarCaSPiS

, a process calculus designed for addressing quantitative aspects of SOC. In order to perform actual model checking, we rely on a dedicated front-end that uses existing state-based stochastic model-checkers, like e.g. the Markov Reward Model Checker (MRMC).

We report on our use of quantitative modelling in predicting the success of systems and services in achieving Service Level Agreements (SLAs). We construct models of the systems in the stochastic process algebra PEPA[1], and queries in the language of eXtended Stochastic Probes (XSP[2]). The query and model together are translated into an underlying continuous time Markov chain (CTMC) which is evaluated in order to assess the SLA. This most often requires a passage-time analysis where a passage (sequence of activity observations) is specified and the numerical analysis returns a function mapping the probability of completing the passage against time since the passage was initiated.

The fluid interpretation of the process calculus PEPA provides a very useful tool for the performance evaluation of large-scale systems because the tractability of the numerical solution does not depend upon the population levels of the system under study. This paper offers a tutorial on how to use this technique by analysing a case study of a service-oriented application to support an e-University infrastructure.

We report on a new style of passage measurement – called passage-end calculations – associated with stochastic probes and their extension to eXtended Stochastic Probes (XSP) [1]. While stochastic probes allow for the analysis of a passage to be split up into several cases depending on the conditions which hold at the start of the passage, even XSP lacks the ability for the same kind of separation depending on conditions at the end of the passage. In particular we would like to separate successful responses to a request from negative responses, timeouts or other failures. This allows us to evaluate refined service level agreements such as: “At least 90 percent of all

successful

requests are responded to within 10 seconds” or “At least 90 percent of all requests are responded to within 10 seconds

and

at least 60 percent of all such requests are successful.” We present a case study in the use of passage-end measurements using a robot bowling demonstration used at the ICT 2008 computer fair, one of Europe’s leading information technology fairs.

We show a number of applications of the tools which have been developed within the

sensoria

project to perform quantitative analysis of services. These tools are formally grounded on source calculi which allow the description of services at distinct levels of abstraction, and hence pose distinct challenges to both modelling and analysis.

The reported applications refer to (suitable subcomponents of) the Finance Case-Study, and show instances of, respectively, exact model checking of

MarCaSPiS

against the both state-aware and action-aware logic SoSL, exact and statistical model checking of sCOWS against the state-aware logic CSL, querying of PEPA models by terms of the XSP language that expresses both state-aware and action-aware stochastic probes.

Sensoria

proposes a model-driven approach for the entire development cycle of services-based applications and infrastructures including the design, formal analysis, deployment and re-engineering of services. This chapter presents the model-driven engineering vision of the project and a summary of achievements to demonstrate the feasibility of the approach. This approach and the challenges in model driven development are illustrated on the example of an end-to-end model transformation chain which bridges BPEL with precise formal model checking technologies and supports the back-annotation of the analysis results directly to the engineering level design model.

Model transformations are a core technology of today’s model-driven software development processes.

Graph transformations

provide a state-of-the-art formalism to specify and execute such transformations in practice. This was the case in the

Sensoria

project, where graph transformations have been used as enabling technology in a number of applications, as well as the basis of research in many topics. In this chapter, we overview the research results that have been achieved in the theory and practice, concentrating on three key areas: (i) the high-level

specification

of transformations, (ii) correctness

analysis

of transformations using formal methods, and (iii) novel event-driven

execution

schemes relying on incremental graph pattern matching technology.

The ability to dynamically compose autonomous services for optimally satisfying the requirements of different applications is one of the major advantages offered by the service-oriented computing (SOC) paradigm. A dynamic service composition implies that services requesters can be dynamically bound to most appropriate service providers that are available at runtime, in order to optimally satisfy the service requirements. At the same time, the autonomy of services involved in a composition means that the resulting composition may need to be adapted in response to changes in the service capabilities or requirements. Naturally, the infrastructure and technologies for providing runtime support for dynamic and adaptive composition of services form the backbone of the above process. In this chapter, we describe the Dino approach for providing the runtime support for dynamic and adaptive service composition. The Dino approach provides comprehensive support for all stages of a service composition life-cycle, namely: service discovery, selection, binding, delivery, monitoring and adaptation.

This chapter presents an overview of the work on migration of legacy systems towards Service-Oriented Architectures that is taking place within the

Sensoria

project. In this context, a general methodology for software reengineering was developed and instantiated in two dimensions to allow service components to be extracted from legacy applications. The main goal of this work is to provide a systematic way of addressing such reengineering projects with a high degree of automation while being largely independent of the programming language. The approach is based on a combination of techniques such as source code analysis, graph transformation, and code transformation. The focus in this text is on the description of the methodology, its dimensions for SOA, a prototype implementation and preliminary results and conclusions.

Developing service-oriented software involves dealing with multiple languages, platforms, artefacts, and tools. The tasks carried out during development are varied as well; ranging from modeling to implementation, from analysis to testing. For many of these tasks, the

Sensoria

project has provided tools aiding developers in their work – with a specific focus on tools based on rigorous formal verification methods, but also including modeling, transformation, and runtime tools. To enable developers to find, use, and combine these tools, we have created a tool integration platform, the

Sensoria

Development Environment (SDE), which a) gives an overview of available tools and their area of application, b) allows developers to use tools in a homogeneous way, re-arranging tool functionality as required, and c) enables users to stay on a chosen level of abstraction, hiding formal details as much as possible. In this chapter, we give an in-depth review of the SDE, integrated tools, and ways of using tools in combination for developing and verifying service-oriented software systems.

A main challenge in

Sensoria

has been the inclusion of case studies from different industrial and academic application areas, namely finance, automotive, telecommunications, and university administration. The case studies, along with a short description of available scenarios, have already been introduced in Chapter 0-3. In this chapter, we go into more detail, presenting the (graphical) specifications for selected scenarios by using the modeling approaches introduced in

Sensoria

. Furthermore, we detail the implementation of demonstrators for some of the case studies.

In this chapter we provide an overview of the application of the results obtained in

Sensoria

(i.e., techniques, methods and languages developed in the technical work packages WP1-WP7) to case studies from the Automotive, eUniversity, Finance and Telecommunication domains (developed in work package WP8).

In this paper, we give a recount of the application of

Sensoria

approaches, languages, and tools to the modeling of movement of the robot that has taken the lead role in

Sensoria

demonstrations at the exhibitions ICT 2008 in Lyon and FET 2009 in Prague. The demos were centred around a robot-bowling game that actively involved the visitors in programming a robot that plays bowling, using some of the techniques developed in

Sensoria

in order to predict the outcomes of the game according to their design choices. Specifically, the

Sensoria

techniques have been used for the analysis of functional and non-functional properties of the system, both in the ex-post analysis of the robot movement during the demo and in the ex-ante analysis of the possible robot configurations during the design of the robot and of the demo itself. This paper presents how the techniques have been applied and to what extent the results of the application match the real robot behavior. The

Sensoria

modeling and analysis techniques used are the UML4SOA graphical modeling language, the Performance Evaluation Process Algebra PEPA, the UMC model checker and the Markovian process algebra MarCaSPiS.

This chapter provides an effective implementation of (part of) the

Sensoria

approach, specifically

modelling

and

formal analysis

of service-oriented software based on mathematically founded techniques. The ‘Finance case study’ is used as a test bed for demonstrating the feasibility and effectiveness of the use of the process calculus COWS and some of its related analysis techniques and tools. In particular, we report the results of an application of a temporal logic and its model checker for expressing and checking functional properties of services and a type system for guaranteeing confidentiality properties of services.

We describe the

Sensoria

development approach using a pattern language for augmenting service engineering with formal analysis, transformation and dynamicity. The pattern language is designed to help software developers choose appropriate tools and techniques to develop service-oriented systems with support from formal methods; the full pattern catalog spans the whole development process from the modeling stage to deployment activities. Some of the patterns are specific to

Sensoria

; other patterns are extensions or adaptations of patterns presented by other authors.