| EPSRC Reference: |
GR/T20106/01 |
| Title: |
Formal Specification and Verification of ARM-Based Systems |
| Principal Investigator: |
Gordon, Professor M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 October 2004 |
Ends: |
30 September 2007 |
Value (£): |
193,684
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
If successful, this project will result in possibly the first machine checked formal verification of software running on a formally verified commercial offthe-shelf (COTS) processor. It will provide data and methodology to enable future system designers to evaluate the costs and benefits of formal proof of correctness as part of their verification flow. As a case study we will develop a demonstrator application written in ARM assembler that communicates over a system bus with one or more co-processors. The demonstrator will explore how mechanised reasoning can increase assurance that information is secure, a property of current commercial significance for devices like mobile phones, PDAs and set top boxes.
|
|
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: |
http://www.cl.cam.ac.uk/~acjf3/arm/ |
| Further Information: |
|
| Organisation Website: |
http://www.cam.ac.uk |