REASONING ABOUT REAL-TIME PROGRAMS USING IDLE-INVARIANT ASSERTIONS
Dr Ian Hayes, Department of Computer Science and Electrical Engineering, University of Queensland, Australia

Abstract: We develop a set of laws for reasoning about real-time programs using assertions (preconditions and postconditions) in the style of Hoare. In the real-time context assertions may refer to the current time and to the value of external inputs, which are not under the direct control of the program and hence not guaranteed to be stable with respect to the passage of time (even if the program does not modify any of the variables under its control). Hence in order to reason about real-time programs, we make use of idle-invariant assertions: assertions that are invariant to just the passage of time.

This seminar was held at the Department of Computer Science, Royal Holloway, University of London on 28 November 2000.

back