Details of Grant 

EPSRC Reference:	EP/C510712/1
Title:	NETSEM: Rigorous Semantics for Real Systems
Principal Investigator:	Sewell, Professor PM
Other Investigators:	Wansbrough, Dr K Gibbens, Dr R
Researcher Co-Investigators:	Dr M Norrish
Project Partners:	National ICT Australia
Department:	Computer Science and Technology
Organisation:	University of Cambridge
Scheme:	Standard Research (Pre-FEC)
Starts:	30 May 2005	Ends:	29 November 2008	Value (£):	282,163
EPSRC Research Topic Classifications:	Fundamentals of Computing Networks & Distributed Systems
EPSRC Industrial Sector Classifications:	Communications
Related Grants:
Panel History:
Summary on Grant Application Form
The existing global information infrastructure is extremely complex. It rests on network protocols (TCP, UDP, IP, with their Sockets API) which provide the low-level services of byte-stream and asynchronous datagram communication; higher-level middleware layers, providing directories, messaging, failure detection, resource allocation, \etc, and programming languages for writing both middleware and applications. The sum is very poorly understood. Consequently, the construction of distributed infrastructure is still a matter of craft, requiring a great deal of specialised experience and painful testing. There has been much (essential) theoretical work on idealised models, but, with some exceptions, it remains far removed from the intricacies of real systems. Our poor grasp of the foundations carries a great risk that the infrastructure we build today will be inadequate for the future: brittle, unreliable, and inefficient.To remedy this state of affairs, we will develop mathematical models of the behaviour of the network protocols and the Sockets API, as they are deployed, that precisely describe both normal behaviour and the many failure and error cases. Our models will be expressed with a higher-order-logic proof assistant (HOL). We aim to make them readily usable by middleware designers and implementors, validating the models against the deployed implementations and drawing feedback from the community. We will integrate the models with programming language semantics, thereby supporting automated reasoning about executable distributed programs, and will use them as a basis for pre-hoc oasign work for future protocols, especially proposals for congestion control based on resource pricing.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.cam.ac.uk