| EPSRC Reference: |
GR/L86180/01 |
| Title: |
LAX LOGIC APPLIED TO FORMAL SYSTEM DESIGN |
| Principal Investigator: |
Fairtlough, Dr M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Sheffield |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
24 August 1998 |
Ends: |
23 May 2002 |
Value (£): |
181,454
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The research involves developing the theory of Lax Logic, implementing it in the LAMBDA tool for formal system design and carrying out a number of case studies. Here Lax Logic refers to a class of logics which are endowed with a single modal operator somehow which gives formal status to the abstraction principle via a notion of correctness-up-to-constraints. During the first two years we will establish a generic constraint handling machinery for a version of Lax Logic that encompasses two abstraction levels. We will undertake three representative case studies which will test our packages for timing, data and structural abstraction. During the third year the results will be refined and extended to deal with a fixed but arbitrary number of abstraction levels, and then applied to the main case study - a formal synthesis of the Amulet asynchronous microprocessor. We expect that the techniques developed by this research will lead to significant economies in the formal design process.
|
|
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.shef.ac.uk |