GLOBAN 2008 Summer School – The Global Computing Approach to Analysis of Systems

Session Centered Calculi for Service Oriented Computing

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.

Declarative Datacentres

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.

Introductory reading:

  • The course materials are available here

Final slides:

Foundations of Model Transformations: A Lambda Calculus for MDD?

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.

Introductory reading:

  • R. Heckel. Graph transformation in a nutshell. In Proceedings of the School on Foundations of Visual Modelling Techniques (FoVMT 2004) of the SegraVis Research Training Network, volume 148 of Electronic Notes in TCS, pages 187-198. Elsevier, 2006. PDF
  • R. Heckel. Stochastic analysis of graph transformation systems: A case study in P2P networks. In H. Dan Van and M. Wirsing, editors, Proc. Intl. Colloquium on Theoretical Aspects of Computing (ICTAC 05), Hanoi, Vietnam, volume 3722 of LNCS. Springer-Verlag, October 2005. Invited paper. PDF

Final slides (including problems and solutions):

Type-based Verification in Global Computing

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.

Introductory reading:

  • Lennart Beringer and Martin Hofmann, Secure information flow and program logics, Proceedings of 20th IEEE Computer Security Foundations Symposium (CSF 07)
  • Lennart Beringer, Martin Hofmann, and Mariela Pavlova, Certification using the Mobius Base Logic PDF
  • Martin Hofmann and Steffen Jost, Type-Based Amortised Heap-Space Analysis Peter Sestoft (Ed.): Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings. Lecture Notes in Computer Science 3924 Springer 2006, ISBN 3-540-33095-X 22-37, PDF

Performance Analysis and Model Checking - A Perfect Match

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.

Introductory reading:

  • Probabilistic Systems, Chapter 10 of "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen, MIT Press, 2008.
  • Stochastic Model Checking by Marta Z. Kwiatkowska, Gethin Norman, David Parker. Formal Methods for Performance Evaluation. Lecture Notes in Computer Science 4486 Springer (2007) 220-270. PDF
  • Perspectives in Probabilistic Verification by Joost-Pieter Katoen, Theoretical Aspects of Software Engineering, IEEE CS Press, page 1-10, (2008). PDF

Final slides:

Verification-centric Software Engineering

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.


  • MOBIUS PVE for Linux
  • MOBIUS PVE for MacOS
  • MOBIUS PVE for Windows
  • Workspace examples
  • Exam assignment - deadline Thursday, September 25, 2008, midnight (i.e. 23:59.(9))

Introductory reading:

  • The course materials are available here


Static Analysis of Services

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.

Final slides:

Information-flow Security

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.

Introductory reading:

The topic is divided in two sets. The respective introductory reading follows:

  • Andrei Sabelfeld and Andrew C. Myers, Language-Based Information-Flow Security, IEEE JOURNAL ON SELECTED AREAS IN COMMUNICATIONS, VOL. 21, NO. 1, JANUARY 2003 1, PDF
  • Andrei Sabelfeld and David Sands, Declassification: Dimensions and Principles, Journal of Computer Security, (c) IOS Press. PDF

Final slides:

Mobility, Ubiquity and Security: Proof-carrying Code for Java on mobile devices

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.

Introductory reading:

SENSORIA: Software Engineering for Service-Oriented Overlay Computers

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.

Introductory reading:

  • Roberto Bruni, Hernan Melgratti, and Ugo Montanari. Theoretical Foundations for Compensations in Flow Composition Languages. In Proc. 32nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL'05), pages 209-220. ACM, 2004.
  • Howard Foster, Philip Mayer. Leveraging Integrated Tools for Model-Based Analysis of Service Compositions. Proceedings of Third International Conference on Internet and Web Applications and Services (ICIW 2008), Athens, Greece, June 8-13, 2008.
  • Philip Mayer, Andreas Schroeder, and Nora Koch. MDD4SOA: Model-Driven Service Orchestration. Proceedings of 12th IEEE International EDOC Conference (EDOC 2008), September 15-19, 2008, Munich, Germany.
  • Martin Wirsing, Allan Clark, Stephen Gilmore, Matthias Hölzl, Alexander Knapp, Nora Koch, and Andreas Schroeder. Semantic-Based Development of Service-Oriented Systems. In E. Najn et al., editor, Proc. 26th IFIP WG 6.1 Internat. Conf. on Formal Methods for Networked and Distributed Systems (FORTE'06), Paris, France, volume 4229 of LNCS, pages 24-45. Springer, 2006.
  • SENSORIA project
  • "MDD4SOA"
  • SENSORIA Whitepaper
  • Presentation of SENSORIA
Valid XHTML 1.1 Valid CSS!