Seventh Asia-Pacific Software Engineering Conference (APSEC'00)
Reasoning about real-time programs using idle-invariant assertions
Singapore
December 05-December 08
ISBN: 0-7695-0915-0
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.
Index Terms:
real-time systems; formal logic; software engineering; real-time program reasoning; idle-invariant assertions; preconditions; postconditions; Hoare logic
Citation:
I. Hayes, "Reasoning about real-time programs using idle-invariant assertions," apsec, pp.16, Seventh Asia-Pacific Software Engineering Conference (APSEC'00), 2000