Projections: A Technique for Verifying Real-Time Programs in Duration Calculus

We present a technique for handling the true synchrony hypothesis and (infinite) loops in realtime programming. The technique is based on the notion of projections and iterations in Duration Calculus. With this technique, the semantics of real-time programs with shared variables is given in a simple way, and the verification can be done using DC proof system. Dang Van Hung is from the Institute of Information Technology of National Center for Natural Science and Technology of Vietnam, where he is a researcher. He was Fellow of UNU/IIST from April 1994 till July 1995. He becomes a Research Fellow of UNU/IIST since Octomber 1995. His research interests include Formal Techniques of Programming, Concurrent and Distributed Systems. E-mail: dvh@iist.unu.edu Copyright c fl 1999 by UNU/IIST, Dang Van Hung Contents i Contents 1 Introduction 1 2 DC 2 2.1 Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Semantics . . . . . . . . . . . . . ..