| EPSRC Reference: |
GR/L68445/01 |
| Title: |
THE INTEGRATION OF TWO INDUSTRIALLY RELEVANT FORMAL METHODS (VDM+B) |
| Principal Investigator: |
Bicarregui, Dr J |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computational Science & Engineering |
| Organisation: |
STFC Laboratories (Grouped) |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
14 September 1998 |
Ends: |
13 March 2002 |
Value (£): |
110,362
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
VDM are among the few formal methods currently in use by industry and supported by commercial tools. Both are model-oriented methods for the development of sequential systems based on first-order-predicate-calculus and set-theory. However, VDM encourages a more implicit style of specification aimed at high-level design and data-refinement, whereas B is more focused on low-level design, algorithm-refinement and code-generation. This difference of focus has lead to different functionality in tool support for the methods. Currently a religious war hinders the uptake of both methods and the establishment of either as the definitive industrial-strength formal method in its domain. Recently approved, the ESPRIT project SPECTRUM brings together commercial suppliers of VDM and B toolkits and industrial users of the two methods to assess the commercial viability of producing integrated support for the two methodologies. The integrated method will be of major significance to users of formal methods but, within that project, there is no provision for investigating the formal basis of the combination. The proposed project will develop the formal underpinnings for the combined method by identifying a core language common to both, developing an axiomatic semantics for it and deriving a set practical proof rules from this.
|
|
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: |
|