Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Coercing Real-Time Refinement: A Transmitter

    1st BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 23rd - 24th September 1996


    I.J. Hayes & M. Utting


    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.


    PDF filePDF Version of this Paper (97kb)