| EPSRC Reference: |
GR/R24081/01 |
| Title: |
Automatic Guidance For the Formal Verification of High Integrity Ada |
| Principal Investigator: |
Ireland, Professor A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
S of Mathematical and Computer Sciences |
| Organisation: |
Heriot-Watt University |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 September 2001 |
Ends: |
31 August 2004 |
Value (£): |
150,427
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
A key challenge identified by Foresight is the need for readier access to formal methods for developers of safety critical systems . Automation will playa crucial role in meeting this challenge. The aim of this project is to investigate techniques for automating the formal verification of software for critical systems. In particular we will focus upon SPARK, a subset of the Ada programming language developed by Praxis Critical Systems. SPARK is used extensively within the production of high integrity software within the finance, areospace, rail and telecommunications markets. Programming in SPARK is supported by a toolkit. The toolkit includes the SPADE Proof Checker, an interactive system that supports the construction of formal verification proofs. Formal verification represents the highest level of analysis that the SPARK toolkit provides and is deemed applicable when dealing with the development of critical systems. The SPADE Proof Checker, however, requires highly skilled users with development times typically measured in person-months. Our aim is to address this bottle-neck by adapting and extending proof planning techniques for use with the SPADE Proof Checker. Proof planning, an extension to tactic based reasoning, has a proven track-record in increasing the level of automation provided by proof checkers. We believe the proof planning techniques can make a significant impact on the SPARK approach to producing high integrity software. We also believe that working on industrial strength problems provided by Praxis will be beneficial to our basic research agenda as well as the wider formal methods community.
|
|
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.hw.ac.uk |