Teaching Module: MOBILE SYSTEM VERIFICATION

____________________________________

COMPUTER SCIENCES [LM-CS]  

Lesson.

28 h

Characterizing training activity

INF/01

4

Understanding the foundations of mobile systems. Learning the basic techniques to describe the form and meaning of mobile systems and to reason about them.  Applying the proposed technique in the context of areas such as operating systems, communication protocols, semantics of concurrent and object-oriented programming languages, i.e. any computing entities which can be described in terms of how communication channels move between them.

Some knowledge - not much, but enough to know the basic ideas - of some process algebra (eg CCS).

A mathematical theory for "mobility" has been developed in the pi-calculus. This calculus proposes the transmission of "names" (atomic access capabilities) from one entity to another as the basic computational steps. For this reason, the pi-calculus will be introduced as a basic paradigm for naturally modeling systems with a changing structure. Topics that will be surveyed include: algebraic theory, behavioral equivalences and preorders, and  automatic analysis tools.

CONTENTS:

Basic concepts: How to model computational phenomena with name-passing. Pictorial and linear pi-calculus syntax and pragmatics.

Semantics:  The transitional semantics of the pi-calculus and some of its properties; Observational semantics based on labels and on reductions; Testing preorders.

Main expressiveness results.

Automatic analysis:  Basic principles of the Mobility Workbench, an automatic tool for the pi-calculus.

Active student participation in the seminars. Completion of a project  for mobile processes (group or individual assignment) at the end of the course.

• R. Milner, J. Parrow and D. Walker. A calculus of Mobile Processes, Part I and II. Information and Computation 199:1-77 (1992).

• R. Milner. The polyadic pi-Calculus: a tutorial. In F. L. Hamer, W. Hrauer and H. Schwichtenberg, editors, Logic and Algebra of Specification. Springer-Verlag (1993).

• J. Parrow and D. Sangiorgi. Algebraic theories for name-passing calculi. Research report R93:04, Swedish Institute of Computer Science (1993).

• B. Victor. A Verification Tool for the Polyadic pi-Calculus. Licentiate Thesis, Department of Computer Systems, Uppsala University (1994).

• B. Victor. The Mobility Workbench User's Guide. Technical Report DoCS 95/xx, Department of Computer Systems, Uppsala University (1995).

• B. Victor and U. Nestmann. Bibliography on Mobile Processes and the pi-Calculus.

Slides.