Refinement Patterns for Contractual Statecharts

Lead Research Organisation: University of York
Department Name: Computer Science


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.
Description A set of repeatable, validated patterns that can be used to build software systems that must respond to requests within a particular time-frame, along with engineering support for applying these patterns.
Exploitation Route Researchers interested in the theory of reactive and real-time systems engineering.
Sectors Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software)

Description The results have been deployed in the Epsilon open-source model management toolkit. They are used in both teaching and in the development of software.
First Year Of Impact 2010
Sector Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software)
Impact Types Societal,Economic

Description Framework 7 Project 2007
Amount € 550,000 (EUR)
Funding ID 218575 
Organisation European Commission 
Sector Public
Country European Union (EU)
Start 10/2008 
End 09/2011
Title Epsilon 
Description An integrated framework of model management tools. Development was started under EC FP6 funding, and was then part-supported by EPSRC and further EC FP7 funding. 
Type Of Technology Software 
Year Produced 2008 
Open Source License? Yes  
Impact Besides over 100 papers being published, the software is used in teaching worldwide, and some of its components have been turned into a product by BAE Systems.