| EPSRC Reference: |
GR/R96859/01 |
| Title: |
Vertication and development of interacting software components |
| Principal Investigator: |
Treharne, Professor H |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Royal Holloway, Univ of London |
| Scheme: |
First Grant Scheme Pre-FEC |
| Starts: |
27 January 2003 |
Ends: |
26 April 2005 |
Value (£): |
114,590
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The project aims are to extend and build on the Principal Investigator and Steve Schneider's results on verifying concurrent combined specifications.A concurrent combined specification is described from two viewpoints, one which describes the state models of the components using the B-Method and the other specifies allowable behaviour patterns using the process algebra of Communicating Sequential Processes. (CSP).The programme will develop prototype tool support in order to automatically generate interfaces for combined components. This enables code generated from the state model to be controlled using the behavioural patterns. The advantage is that the interfaces will always preserve the integrity of the state model with respect to its safety properties. Furthermore, this will allow an interface of a formally developed component to become a plug-in piece of software in a larger system. The other area of work will involve extending the theoretical results to allow for the specification and verification of temporal properties of combined systems and to allow for model checking large systems. Two case studies will be used during the project to evaluate the tool support and inform the theoretical developments.
|
|
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: |
|