| EPSRC Reference: |
GR/N05963/01 |
| Title: |
INTEGRATING SEQUENTIAL AND CONCURRENT VERIFICATION TECHNIQUES FOR HIGH INTEGRITY REAL-TIME SOFTWARE |
| Principal Investigator: |
Burns, Professor A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of York |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 September 2000 |
Ends: |
30 September 2003 |
Value (£): |
172,752
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
| Aerospace, Defence and Marine |
Manufacturing |
| Chemicals |
Information Technologies |
| Transport Systems and Vehicles |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
This research proposal is aimed at integrating sequential, concurrent and temporal verification. The SPARK system will be used as a demonstrator of a sequential verification capability. The concurrency model is defined by the Ravenscar profile recently specified for hard real-time systems. Timing analysis will make use of path analysis and will investigate the use of Linear Programming tools. Scheduling analysis will be based on fixed priority-based scheduling as developed at the University of York. Model checking will be used to verify key aspects of any concurrent system structured according to the Ravenscar profile. Sequential verification techniques make simplifying assumptions about the environment in which they execute. Such techniques must therefore be re-evaluated/modified if verification of the complete concurrent system is to be achieved. The success of the proposed research will be demonstrated by adapting SPARK to the Ravenscar concurrency profile and by extending SPARK verfification capability to include: timing analysis, model checking and scheduling.
|
|
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.york.ac.uk |