Coercing real-time refinement: a transmitter

Our overall goal is to support the development of real-time programs from specifications via a process of stepwise refinement. One problem in developing a real-time program in a high-level programming language is that it is not possible to determine the detailed timing characteristics of the program until the compiler and target machine are taken into account. To overcome this problem the programming language can be augmented with directives specifying real-time constraints; it is a compile-time error if the compiler cannot guarantee that the generated code will meet them. During the refinement process the timing directives are inserted into the program in order to ensure it meets the specification. The paper introduces the real-time directives, gives a set of laws for real-time refinement, and illustrates their use in the refinement of a simple real-time transmitter