TY - JOUR AB - 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, which are discussed elsewhere in this volume. AU - Alur, Rajeev AU - Henzinger, Thomas A ID - 4584 IS - 1-2 JF - Software Tools For Technology Transfer SN - 1433-2779 TI - Real-time system = discrete system + clock variables VL - 1 ER -