Seminar: Global Computing

Winter Semester 2005/06
Lehrstuhl fr Informatik 2

Diplomstudiengang Informatik
(Theoretische Informatik, Vertiefungsfach "Formale Methoden, Programmiersprachen und Softwarevalidierung")
Master Programme Software Systems Engineering
(Theoretical CS, Specialisation Subject "Formal Methods, Programming Languages and Software Validation")

Contents

1. Decentralized control: they are composed of autonomous computational entities (also called agents) whose activities are not centrally controlled (e.g., as global control is impractical, or because the agents have different owners).
2. Mobility: of the physical platforms or of the agent (from one platform to another).
3. High dynamics: the system configuration may vary over time, e.g., new agents (or platforms) may be dynamically created or deleted. The agents' behaviour may also vary over time.

The aim of this seminar is to provide insights into the problems of the design and construction of global computing systems. We thereby focus on formal methods, i.e., mathematically rigorous techniques and tools for the specification, design and verification of global computing systems. This includes techniques such as type systems, process algebras, modelling languages and state-of-the-art programming languages and environments.

For more details we refer to Cardelli's seminal paper Global Computation.

Prerequisites

• Vordiplom or Bachelor in Computer Science and
• basic knowledge in models for concurrent and/or mobile systems as acquired in courses such as
• Probabilistic Models for Concurrency or
• Formal Models of Concurrency.

Registration

Introduction

Results of the questionnaire for the Global Computing seminar

Topics

Thursday, 8:15am, at the seminar room of I2.

Literature

[Mil99]

Robin Milner: Communicating and Mobile Systems: The pi-Calculus, Cambridge University Press, 1999

[Par01]

Joachim Parrow: An Introduction to the pi-Calculus, In Handbook of Process Algebra, ed. Bergstra, Ponse, Smolka, Elsevier 2001, pp. 479-543

[Car00]

Luca Cardelli: Mobility and Security. Lecture notes for Marktoberdorf Summer School 1999 , Foundations of Secure Computation, Friedrich L. Bauer et al (Eds.), NATO Science Series, Proceedings of the NATO Advanced Study Institute on Foundations of Secure Computation, Marktoberdorf. IOS Press, 2000. pp. 3-37.

[CG00]

Luca Cardelli, Andrew D. Gordon: Mobile Ambients, Theor. Comput. Sci. 240(1): 177-213 (2000)

[BCC04]

Michele Bugliesi, Giuseppe Castagna, Silvia Crafa: Access control for mobile agents: The calculus of boxed ambients , ACM Trans. Program. Lang. Syst. 26(1): 57-124 (2004)

[LS03]

Francesca Levi, Davide Sangiorgi: Mobile safe ambients, ACM Trans. Program. Lang. Syst. 25(1): 1-69 (2003)

[CVZ05]

Giuseppe Castagna, Jan Vitek, Francesco Zappa Nardelli: The Seal Calculus, Information and Computation, to appear

[BBN03]

Lorenzo Bettini et al: The Klaim Project: Theory and Practice, GC 2003, LNCS 2874, Springer, 2003, pp. 88-150

[BN05]

Lorenzo Bettini, Rocco De Nicola: Mobile Distributed Programming in X-Klaim, SFM 2005, LNCS 3465, pp. 29-68

[BKKSW03]

Hubert Baumeister, Nora Koch, Piotr Kosiuczenko, Perdita Stevens, Martin Wirsing: UML for Global Computing, GC 2003, LNCS 2874, pp. 1-24

[CC03]

Luis Caires, Luca Cardelli: A spatial logic for concurrency (part I), Inf. Comput. 186(2): 194-235 (2003)

[CC04]

Luis Caires, Luca Cardelli: A spatial logic for concurrency (part II), Theor. Comput. Sci. 322(3): 517-565 (2004)

[NL04]

Rocco De Nicola, Michele Loreti: A modal logic for mobile agents, ACM Trans. Comput. Log. 5(1): 79-128 (2004)

[NL05]

Rocco De Nicola, Michele Loreti: MoMo: A modal logic for reasoning about mobility , FMCO 2004, LNS, Springer, to be published

[NHN03]

Flemming Nielson, Rene Rydhof Hansen, Hanne Riis Nielson: Abstract interpretation of mobile ambients, Sci. Comput. Program. 47(2-3): 145-175 (2003)

[NNH02]

Flemming Nielson, Hanne Riis Nielson, Rene Rydhof Hansen: Validating firewalls using flow logics, Theor. Comput. Sci. 283(2): 381-418 (2002)

[LB04]

Francesca Levi, Chiara Bodei: A Control Flow Analysis for Safe and Boxed Ambients, ESOP 2004, LNCS 2986, pp. 188-203

Further Resources

• How to write the manuscript (in German)
• A manuscript template (in German)
• How to give the talk (in German)
• For printed slides: seminar.sty
• For video projections: prosper.sty

Contact