Refinement Patterns for Contractual Statecharts

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.