| EPSRC Reference: |
GR/H11471/01 |
| Title: |
THE PRACTICAL APPLICATION OF FORMAL METHODS TO HIGH INTEGRITY SYSTEMS ( IED4/1/9013) |
| Principal Investigator: |
Gollmann, Dr D |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Royal Holloway, Univ of London |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
22 September 1992 |
Ends: |
21 April 1996 |
Value (£): |
89,445
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
| Aerospace, Defence and Marine |
Information Technologies |
| Technical Consultancy |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The project aims to provide guidelines of a cost effective approach using formal methods in the development and assessment of high integrity software systems. The project also aims to devise a methodology and calculus for constructing provably coherent system specifications.Progress:The project is based upon a real-world, mature, case-study. Progress can be seen against three tiers of work: 1. Coherent SpecificationsSeveral logics for formalizing and analyzing requirements have been investigated. The case study has been specified using higher order logic supported by the PVS proof checker. We are currently updating these specifications and proceeding with verification of safety properties.2. Formal DevelopmentThis work is focused upon the cost effective use of currently available tools to support a formal development process. The project is currently carrying out diverse developments, based upon B and VDM, in order to provide cost comparisons. 3. Risk EngineeringThis work has focused upon the integrated use of formal methods to support traditional risk analysis techniques such as fault trees. The work is currently considering the use of coloured petri-nets to model the real-time operation and analysis of high integrity systems.
|
|
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: |
|