Project Descriptions

Title: Liveness and Safety Guarantee by Type Checking of Mobile Processes

Supervisor: Nobuko Yoshida

Prequisites

This project requires knowledge of concurrency programming, types and semantics in general. In particular (a bit of) knowledge of process algebra such as FSP (Finite State Processes) taught in Concurrency Programming course, CCS, CSP or the pi-calculus is required. It is also recommended that a student doing this project should also take Models of Concurrent Computation , Compilers and Type Systems for Programming Languages .

Aims of Project

In distributed systems, the correctness of concurrent programs or systems has been often classified using two terms: the safety and liveness properties. Intuitively a safety property asserts that nothing bad happens during execution of programs, while a liveness property asserts that something good eventually happens. It is well-known that the typing systems of the programming languages can offer a static verification technique to guarantee safety properties.

This project investigates and implements a type-checking system to guarantee not only safety but also liveness in concurrent mobile computing.

This project is built-on a recent study of liveness in mobile computing. During your project, you will be able to learn a powerful concurrent formalism called the pi-calculus . (Recently the pi-calculus is used to design a shipping server product, the XLang Scheduler in Microsoft BizTalk Server 2000 . Also the pi-calculus was introduced as a key formal model for XML in a major XML text book, Professional XML 2nd Edition, Wrox Press 2001).

Thus this project is very challenging and fun because you can learn both the pi-calculus (advanced theory) and type-checking (implementation).

Learning Outcomes

To learn about type-checking of mobile processes.
To specify, design and implement a type-checker to guarantee liveness and safety.

Project Timetable

Term 1

To learn about concurrent mobile processes; to learn about type-checking; to specify and design a type-checker.

Term 2

Implementation of the type-checker.

References

Available from Nobuko Yoshida (yoshida@doc.ic.ac.uk).
http://www.doc.ic.ac.uk/~yoshida/ (click secure information analysis and typing systems for concurrent computation and programming ).

Calculi for Mobile Processes