| EPSRC Reference: |
GR/J18682/01 |
| Title: |
SAFETY CRITICAL REVALIDATION IN THE PROCESS INDUSTRY - IED4/1/9317 |
| Principal Investigator: |
Bennett, Professor K |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Engineering & Computer Science |
| Organisation: |
Durham, University of |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 May 1994 |
Ends: |
31 January 1998 |
Value (£): |
217,893
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The fundamental problem addressed in this project is the reverse engineering of real-time process control software, focusing particularly on timing and concurrency issues, to allow its safety properties to be audited and assessed more easily. This project draws on previous work, conducted both at the University of Durham and at Durham Software Engineering Ltd, into the reverse engineering of existing code using formally-proven transformations on a wide spectrum language (WSL), and recent theoretical work on the analysis of real-time and concurrent programs. The first aspect of the project is to extend further these areas of work to facilitate safety analysis. A prerequisite for successful reverse engineering is a language, or notation, in which the results can be expressed, which permits a better representation than the original code. The design of such a language is the second aspect of the project. Progress:The Bylands project has now been running for nine months. So far the work has concentrated on reviewing the field, generating ideas and investigating possible approaches. Discussions with our uncles have provided a clear focus for the project and its application in automatic welding systems. To make WSL more suitable for use with real-time process control software it must be extended to incorporate both real-time and concurrency. Extensions could take the form either: a) as definitional extensions to the language in which new constructs are defined in terms of existing ones, orb) extension of the kernel language to include a suitable formalism such as metric temporal logic.Both approaches are currently being assessed. A formalisation of true concurrency requires an operational semantics for the WSL language to supplement the present denotational semantics, and the development of this is under way. In addition, an appropriate notion of program equivalence, and formal abstract representations for concurrent systems are required; existing formal approaches to concurrency are being investigated and at present the CCS formalism appears to possess many appropriate characteristics.The approach that is being adopted for the representation of reverse-engineering code is to use formally- defined domain-oriented languages. Concepts from the domain (such as objects and time) will appear in the language and operations on these concepts will be available as language constructs. Even though the implementations of these objects and operations could be large and complex, they would have simple representations in the language and would be intuitive to a domain expert. Software validation will be performed informally be a domain expert analysing the system as expressed in the language, while software verification will be performed formally on the formal language definition in terms of WSL.
|
|
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: |
|