| EPSRC Reference: |
GR/K26769/01 |
| Title: |
TAKING ADVANTAGE OF MODULARITY ON FORMAL SYSTEMS DEVELOPMENT |
| Principal Investigator: |
Fitzgerald, Professor J |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Victoria University of Manchester, The |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
30 August 1994 |
Ends: |
29 August 1996 |
Value (£): |
16,129
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
1. Improve the practical applicability of formal methods by developing techniques to exploit modularity and thus reduce the complexity of refinement proofs.2. Define refinement proof obligations in the context of modular specifications.3. Illustrate the above via a body of examples derived from commercial projects.Progress:It is intended to research refinement techniques which are of practical value in problems of a commercial scale, so the majority of work so far has focused on specifications derived from industrial examples. A smaller proportion of time has been devoted to considering refinement of modular specifications of a textbook size. As a result, two studies are in preparation and are intended for publication later in 1995:1. The investigator has been involved in work on the validation of critical safety properties on a large formal model of a nuclear waste tracking system. The validation was hindered by a mixture of reusable generic material in the specification with more application-specific definitions. It is intended to produce a modular generic version of the specification and use it as the basis of an example formal development.2. Previous work in the early 1990s was stimulated by the example of the specification of the IBM Non-programmer Data Base (NDB). This study will investigate whether the refinement strategy adopted for the original flat specification can be applied to the modular version, and if it can, how that affects the statement and discharging of proof obligations.A number of opportunities to present and discuss this work have arisen. An invitation has been received to the First International Conference on Formal Specification: Foundations, Methods, Tools and Applications (FMTS95) in Poland in May 1995, when it is hoped to present the NDB study. An invitation has also been received to the International Conference and Research Centre for Computer Science in Schloss Dagstul on Methods for Semantics and Specification . Informal arrangements have been made for visits in the later part of 1995 to the Laboratory for the Foundations of Computer Science at Edinburgh University, to discuss the formal proof of conjectures in the context of modular specifications; and to the Software Verification Research Centre at the University of Queensland.
|
|
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: |
|