| EPSRC Reference: |
GR/M37493/01 |
| Title: |
LINKING THEORIES WITH TOOLS FOR SYSTEM DEVELOPMENT |
| Principal Investigator: |
Woodcock, Professor JCP |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Oxford |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 July 1999 |
Ends: |
30 June 2002 |
Value (£): |
196,153
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The Z specification method has shown how requirements can be captured formally as alphabetised predicates, describing properties and behaviour of the delivered product. The schema calculus then provides an algebra for refinement of the specification into high-level designs,and the eventual code in a conventional programming language. Recent research in unifying theories of programming has shown that this topdown methodology extends smoothly to other computational paradigms. These formalise concepts relevant to the design of critical systems, e.g. real time, resources, distribution and communication.Within the framework of a mature general purpose symbolic proof system, we propose to implement a structured library of tools supporting a small family of linked theories. This will include optimisations within each theory, transformations between theories, and the generation and discharge of verification conditions at each step of the design. The library will be exercised on standard publishable case studies.We will try to make it easy for implementors and/or users of other more advanced or more specialised tools (e.g. model checkers) to contribute to the common tolkit; and also encourage implementation of more application-oriented theories within the family.
|
|
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.ox.ac.uk |