EPSRC Reference: |
EP/E034853/1 |
Title: |
Refinement Patterns for Contractual Statecharts |
Principal Investigator: |
Paige, Professor R |
Other Investigators: |
|
Researcher Co-Investigators: |
|
Project Partners: |
|
Department: |
Computer Science |
Organisation: |
University of York |
Scheme: |
Standard Research |
Starts: |
01 July 2007 |
Ends: |
30 September 2010 |
Value (£): |
398,273
|
EPSRC Research Topic Classifications: |
Design of Process systems |
Fundamentals of Computing |
Software Engineering |
|
|
EPSRC Industrial Sector Classifications: |
Aerospace, Defence and Marine |
Information Technologies |
|
Related Grants: |
|
Panel History: |
|
Summary on Grant Application Form |
Increasingly, aerospace systems such as airplane engines have a substantial computer software component. Building such software is challenging, because the software must interact with mechanical devices , like sensors on an airplane wing, and with computer hardware. Moreover, this software must be reliable, robust, and above all, safe, i.e., it must be certified as acceptably safe for use. In building such software, engineers typically rely on ad-hoc design methods for control systems. These methods usually start with an abstract description of a proposed solution, expressed in several different styles: operational (describing steps to be taken) and declarative (describing properties that the software should possess). These descriptions are then step-by-step refined into executable programs.The aim of this project is to put this ad-hoc design method on to a formal footing, via the introduction of a new concept called a refinement pattern. A refinement pattern effectively captures the step-by-step refinements that engineers carry out in practice. We will provide formal, mathematical foundations for refinement patterns and for reasoning about refinements. We also intend to support this method by developing novel and specialised tools, including a specialised model checker, that integrate with the widely used Matlab/Stateflow design tool. This will help engineers produce more reliable, more robust aerospace systems by building on their established practices.
|
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.york.ac.uk |