| EPSRC Reference: |
GR/N01132/01 |
| Title: |
COMBINING FORMAL APPROACHES FOR THE ANALYSIS AND VERIFICATION OF NETWORK PROTOCOLS |
| Principal Investigator: |
Sinclair, Dr JE |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Warwick |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 November 2000 |
Ends: |
31 July 2004 |
Value (£): |
52,853
|
| EPSRC Research Topic Classifications: |
| Networks & Distributed Systems |
|
|
| EPSRC Industrial Sector Classifications: |
| Communications |
No relevance to Underpinning Sectors |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Network protocols are an increasingly important aspect of the correct operation of many computer systems. Their use in secure or safety-critical contexts, such as electronic commerce or distributed control systems, requires dependability. Considerable progress has been made in formally verifying certain aspects of protocol behaviour. However, such protocols typically require analysis of a combination of properties, some of which (eg deadlock-freedom) may best be described in event-based terms while others (eg routing tables) are most naturally accommodated by referring directly to system state. We propose to investigate the way in which two formal approaches, exemplifying event-based and state-based specifications respectively, can be used together in a theoretically sound yet practical manner to specify complementary views of a system which may be reconciled at the semantic level. The work is aimed at providing a useable development method in which key properties are specified and proved in an appropriate and natural context, with existing tool support employed where possible. The emphasis of the work is on bringing together several current strands of research and applying it to industrial-strength applications. It will be carried out in co-operation with members of RAL who have extensive experience in the design and implementation of communications protocols.
|
|
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.warwick.ac.uk |