EPSRC logo

Details of Grant 

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:
Software Engineering
EPSRC Industrial Sector Classifications:
Information Technologies
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: