|
|
|
|
Teaching Material - Formal Approaches for Service-Oriented Computing |
|
- Fundamentals of Session Types (slides)
Lectures by Vasco T. Vasconcelos, University of Lisbon, Portugal
9th International School on Formal Methods for the Design of Computer, Communication and Software Systems:
Web Services (SFM-09:WS), 1-6 June, 2009, Bertinoro, Italy
Abstract We present a reconstruction of session types in a linear pi calculus where types are qualified as linear or unrestricted. Linearly qualified communication channels are guaranteed to occur in exactly one thread, possibly multiple times. In our language each channel is characterised by two distinct variables, one used for reading, the other for writing; scope restriction binds together two variables, thus establishing the correspondence between the two ends of a same channel. This mechanism allows a precise control of resources via a linear type system. We build the language gradually, starting from simple input/output, then adding choice, recursive types, replication and finally subtyping. We also present an algorithmic type checking system. - A Formal Approach to Service-Oriented Modelling (slides, movie, paper)
Lectures by José Fiadeiro, University of Leicester, UK
9th International School on Formal Methods for the Design of Computer, Communication and Software Systems:
Web Services (SFM-09:WS), 1-6 June, 2009, Bertinoro, Italy
Abstract This tutorial provides an overview of a formal approach to service-oriented modelling developed within the SENSORIA project. A modelling language – SRML – and a number of formal techniques that address qualitative and quantitative analysis support this approach, all of which are based on mathematical foundations. The focus of the tutorial is on the language primitives that SRML offers for modelling business services and activities, and on the methodological approach that SRML supports. - Session Centered Calculi for Service Oriented Computing (slides, more slides)
Lectures by Rocco De Nicola, University of Florence, Italy 2nd International Summer School on the Global Computing Approach on Analysis of Systems (GLOBAN 2008), September 22-26, Warsaw, Poland
Abstract 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.
- Synchronised Hyperedge Replacement as a Model for Service Oriented Computing (slides, notes)
Lectures by Emilio Tuosto, University of Leicester, UK
Int. PhD School in Theory and Practice of Business Process Execution and Service Orientation, October 16-19, 2007, Copenhagen, Denmark
Abstract This tutorial course will present a framework for modelling a few aspects of distributed computing based on Synchronised Hyperedge Replacement (SHR), a graph rewriting formalism. The SHR framework has been equipped with many formal devices for representing complex synchronisation mechanisms which can tackle mobility, heterogeneous synchronisations and non-functional aspects, key factors of Service Oriented Computing (SOC). We will revise the SHR family as a suitable model for contributing to the formalisation of SOC systems. - Models and Calculi for Security (slides)
Lectures by Massimo Bartoletti of the Universita' degli Studi di Cagliari, Italy, Chiara Bodei, Pierpaolo Degano and Gian Luigi Ferrari of the Universita' di Pisa, and Roberto Zunino of the Universita' degli Studi di Trento, Italy
PhD Course on Models and Calculi for Security, September 17-26, 2007, Pisa, Italy
Abstract This series of lectures gives an overview about security issues in Service-Oriented Computing. The first part of these lectures is devoted to security protocols. We start with a broad introduction to security models and techniques, and we discuss computational versus formal security. Then, we present introduce some of the most relevant security protocols, which we show how to formalise in the pi-calculus, and how to analyse with Control Flow Analysis techniques. We briefly describe Control Flow Analysis techniques for detecting type flaws in Web Services. In the second part of the lectures, we focus on language-based security. After a general overview of the area, we detail a specific framework for controlling resource usage of services, and for implementing service orchestrators based on a call-by-contract primitive.
- Process Algebras and Concurrent Systems (slides)
Lectures by Rocco De Nicola, University of Florence, Italy 1st International Summer School on the Global Computing Approach on Analysis of Systems (GLOBAN 2006), September 22-26, Lyngby near Copenhagen, Denmark Abstract Critical aspects of concurrent systems are related to interaction problems instead of (sequential) computation problems. Process calculi are useful mathematical abstractions that, by focusing on process interaction, can facilitate the analysis of concurrent programming languages and the development/understanding of new programming paradigms. The lectures aim at promoting process calculi as a useful framework for the specification, verification and analysis of concurrent (distributed and mobile) systems.
- Equality of Processes: Equivalences and Proof Techniques (slides)
Lectures by Davide Sangiorgi, University of Bologna, Italy 1st International Summer School on the Global Computing Approach on Analysis of Systems (GLOBAN 2006), September 22-26, Lyngby near Copenhagen, Denmark
Abstract A fundamental concern in concurrency theory is establishing when two processes are "the same", i.e., undistinguishable to an external observer interacting with them. This notion, called, behavioural equivalence, is the basis upon which a theory of processes can be developped. In the lectures the main forms of behavioural equivalence are reviewed. The focus is on bisimulation, for its importance and mathematical properties. In particular, the bisimulation proof method is discussed. This is an instance of a general proof technique called co-induction that is today widely used also outside concurrency theory.
- Type Systems (slides)
Lectures by Vasco Vasconcelos, University of Lisbon, Portugal
1st International Summer School on the Global Computing Approach on Analysis of Systems (GLOBAN 2006), September 22-26, Lyngby near Copenhagen, Denmark
Abstract The well-known benefits of type systems for sequential languages apply to concurrent, distributed languages as well: the partial specification of applications, the early identification of potential runtime errors, the imposition of a programming discipline, the uncovering of important information for compilers. The lectures concentrate on type systems for process calculi that are likely to become more relevant to Service Oriented Computing, starting from the simple type system, through the linear type system, to session types.
|
|
|
 |
|
