EPSRC logo

Details of Grant 

EPSRC Reference: GR/M92188/01
Title: LINKING TOOLS WITH THEORIES
Principal Investigator: Woodcock, Professor JCP
Other Investigators:
Hoare, Professor Sir C Hoare, Professor C
Researcher Co-Investigators:
Project Partners:
Department: Computer Science
Organisation: University of Oxford
Scheme: Standard Research (Pre-FEC)
Starts: 16 July 1999 Ends: 15 July 2000 Value (£): 5,122
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 codes 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 (Isabelle/HOL), we are implementing a structured library of tools supporting a small family of linked theories. This will assist in generation and discharge of verification conditions at each step of the design. The library will be exercised on standard publishable case studies the steam boiler and the smart card.Professor He's visit will enable him to consult on current and future developments of the tool based on his unifying theories, and advise on application to the agreed case studies. He will write a report on his visit.
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