Within the European project SENSORIA, we are developing formalisms for service description that lay the mathematical basis for analysing and experimenting with components interactions, for combining services and formalising crucial aspects of service level agreement. We shall present the outcome of the project by first introducing the basic notions of process calculi, then discussing pi-calculus and finally concentrating on CASPIS, a calculus inspired by pi calculus but with explicit notions of service definition, service invocation, bi-directional sessioning and handling of (unexpected) session closures.

Websites for search, mail, and social networking, for example, are programs running on computers consisting of multiple data centres distributed around the globe. By using techniques such as hardware virtualization, management of these global computers is becoming largely a programming problem. These lectures will describe various declarative approaches to the problem, including techniques based on typed service combinators for achieving reliability and security.

At the heart of any model-driven development process are activities like maintaining consistency, evolution, translation, and execution of models. These are examples of model transformations. A (mathematical) foundation is needed for studying issues like the expressiveness and complexity, execution and optimisation, well-definedness and semantic correctness of transformations. This lecture is about graph transformations as one such foundation.

After introducing the basic concepts of graph transformation by means of an example, applications of graph transformation to model transformation within the Sensoria project will be discussed. This will include an illustration of pair and triple graph grammars for bi-directional transformations, and the problem of compatibility between model transformations and operational semantics.

Type systems are a particular form of modular program analysis which separates correctness of the analysis from the algorithmic task of automation. This makes them particularly suitable for certification of programs from untrusted and potentially even malicious providers.

In the MOBIUS project (WP2 on type-based verification) type systems for various security properties arising in global computing, in particular security of information flow and adherence to resource policies have been developed.

My lectures will survey these results and explain the design and application of type systems in the global computing domain at large.

Whereas model checking focuses on the absolute correctness, in practice such rigid notions are hard, or even impossible, to guarantee. Instead, systems are subject to various phenomena of stochastic nature, such as message loss or garbling, unpredictable environments, faults, and delays. Correctness thus is of a less absolute nature. Accordingly, instead of checking whether system failures are impossible, a more realistic aim is to establish, e.g., whether ``the chance of shutdown occurring is at most 0.01%''. Such queries can be checked using model checking, a technique that enjoys a rapid increase of interest from different communities. Applications from distributed computing, planning and AI, biological process modeling, quantum, and global computing have been tackled with this technique.

But: how does this technique actually work? This talk surveys the foundations of probabilistic model checking, its algorithms, presents some state-of-the-art tools, gives insight into its efficiency, and discusses in detail some of the main recent advances in this field, such as abstraction, state space reduction, counterxample generation, and the treatment of nondeterminism.

This series of talks focus on the practical aspects of designing, constructing, and validating global computing software systems. A suite of robust academic tools, many of which were developed under the EU FP6 MOBIUS project, which are part of the MOBIUS Program Verification Environment (PVE), are summarized and demonstrated.

The first talk gives an overview of the tools options available today, including tools used in this series of talks and others. The second talk focuses on the practical aspects of designing systems for verification. The third talk focuses on refining designs into implementations and validating those designs and refinements via various static checking techniques and automated testing. The final talk focuses on using interactive and automatic theorem provers to perform full functional verification.

Static Analysis has its origins in improving the efficiency of interpreters and compiled code but is gaining increased importance due to its ability to validate important aspects of systems behaviour. For several years static analysis have been used to analyse process algebras for a variety of communication and mobility paradigms in order to establish communication invariants and correctness of communication protocols. A new challenge arises from the use of process algebras for modelling services - ensuring for example that service invocations do not interfere with each other. In these lectures we provide the foundations for performing static analysis for proces algebras including considerations of correctness, adequacy and complexity and touching upon the distinction between compositionality and characteristics.

Information-flow security is concerned with controlling the flow of information through computing systems. These lectures overview recent highlights in the area, including declassification policies and programming language-level information-flow security enforcement mechanisms.

Mobius is a European Integrated Project developing novel technologies for trustworthy global computing, using proof-carrying code to give users independent guarantees of the safety and security of Java applications for their mobile phones and PDAs.

Global computing means that applications today may run anywhere, with data and code moving freely between servers, PCs and other devices: this kind of mobility over the ubiquitous internet magnifies the challenge of making sure that such software runs safely and reliably. In this context, the Mobius project focuses on securing applications downloaded to the Java MIDP platform globally deployed across a host of phones, this is the common runtime environment for a myriad mobile applications.

Techniques of static analysis make it possible to check program behaviour by analysing source code before it ever executes. But mobile code mean that this assurance must somehow travel with the application to reach the user. Conventional digital signatures use cryptography to identify who supplied a program; the breakthrough of proof-carrying code is to give mathematical proofs that guarantee the security of the code itself. We can strengthen digital signatures with digital evidence.

Service-Oriented Computing is an emerging paradigm where services are understood as autonomous, platformindependent computational entities that can be described, published, categorised, discovered, and dynamically assembled for developing massively distributed, interoperable, evolvable systems and applications. Various approaches to engineering service-based systems are in use today; however, critical problems concerning among others automated composition, performance, security and safety, are still not solved satisfactorily, requiring more fundamental studies ranging from essential research questions to practical development and deployment issues.

In order to address these challenges, the IST-FET Integrated Project SENSORIA aims at 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 semiautomatic development and deployment of self-adaptable (composite) services.

In this lecture, the SENSORIA approach to the development of service-oriented systems will be presented. This includes a new generalised concept of service, new semantically well defined modelling and programming primitives for services, new powerful mathematical analysis and verification techniques for assessing system behaviour and quality of service properties, and a suite of tools supporting model-based transformations, development, and deployment of service-oriented systems as well as reengineering legacy software into services.