EPSRC logo

Details of Grant 

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:
Wellings, Professor A
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:
Software Engineering
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