|
| EPSRC Reference: |
GR/R76950/01 |
| Title: |
Mathematical Models for Concurrent and Mobile Computation |
| Principal Investigator: |
Dr I Stark |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
Sch of Informatics |
| Organisation: |
University of Edinburgh |
| Scheme: |
Advanced Fellowship |
| Starts: |
01 July 2002 |
Ends: |
30 June 2007 |
Value (£): |
246,763
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
20 Nov 2001
|
Technology Fellowships Sift Panel
|
Deferred
|
|
|
Summary |
|
The overall aim of this research is to develop and refine mathematical models for concurrent computation, and in particular for features arising from locations, distribution and mobility of both data and computation. Such models provide a powerful way to explore the properties of these features, and cast light on the nature of distributed computation. The project comprises three interdependent strands: to refine existing models for process calculi; to investigate new mathematical constructions to model location, mobility and distribution; and to extract novel logical systems and reasoning methods from such models.
|
| Final Report Summary |
The overall aim of this research is to develop and refine mathematical models for interacting programs, and in particular for features that arise from naming, location, and mobility of both data and computation.
Mathematical models help us to understand the behaviour of complex systems: by providing a language to describe such systems, and potentially tools to analyse and predict that behaviour.
In this project the complexity arises from trying to reason about programs that connect with each other in order to communicate; that change those connections; and that move from one computer to another.
The specific objectives of the project deal with three linked areas: the pi-calculus, an established system for describing concurrent computation; names and the binding of names to values; and use of machine-checked proofs as guarantees of program behaviour.
This last area, "proof-carrying code", has a direct practical use in providing security certificates for Java applications. Proof-carrying code complements existing digital signatures: where those tell us who supplied a program, mathematical proofs can guarantee the behaviour of the code itself.
|
| Further Information: |
|
| Organisation Website: |
http://www.ed.ac.uk |
|
|