loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
I. Hayes, Sch. of Comput. Sci. & Electr. Eng., Queensland Univ., Brisbane, Qld., Australia
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
Usage of this product signifies your acceptance of the Terms of Use.