Rajeev Alur and Thomas A. Henzinger
Programs such as device drivers and embedded controllers must explicitly refer and react to time. For this purpose, a variety of language constructs--including delays, timeouts, and watchdogs--have been put forward. We advocate an alternative proposal, namely, to designate certain program variables as clock variables. The value of a clock variable changes as time advances. Timing constraints can be expressed, then, by conditions on clock values. A single new language construct--the guarded wait statement--suffices to enforce the timely progress of a program. We illustrate the use of clock variables and guarded wait statements with real-time applications such as round-robin (timeout-driven) and priority (interrupt-driven) scheduling. Clock variables generalize naturally to variables that measure environment parameters other than time. This observation leads to a language for hybrid (mixed digital-analog) applications such as embedded process control.
This paper introduces, gently but rigorously, the clock approach to real-time programming. We present with mathematical precision, assuming no prerequisites other than familiarity with logical and programming notations, the concepts that are necessary for understanding, writing, and executing clock programs. In keeping with an expository style, all references are clustered in bibliographic remarks at the end of each section. The first appendix presents proof rules for verifying temporal properties of clock programs. The second appendix points to selected literature on formal methods and tools for programming with clocks. In particular, the timed automaton, which is a finite-state machine equipped with clocks, has become a standard paradigm for real-time model checking; it underlies the tools HyTech, Kronos, and Uppaal, discussed elsewhere in this volume.
Software Tools for Technology Transfer 1:86-109, 1997. A preliminary version appeared in Theories and Experiences for Real-Time System Development (T. Rus, C. Rattray, eds.), AMAST Series in Computing, Vol.~2, World Scientific, 1994, pp. 1-29.