Reasoning about real-time repetitions: terminating and nonterminating

It is common for a real-time system to contain a nonterminating process monitoring an input and controlling an output. Hence, a real-time program development method needs to support nonterminating repetitions. In this paper we develop a general proof rule for reasoning about possibly nonterminating repetitions. The rule makes use of a Floyd

• Type: Journal
• Year: 2002
• Where: SCP
• Authors: Ian J. Hayes
• Keywords: General Proof Rule, Nonterminating Repetitions, Real-time Program Development, SCP 2002