Formal Design of Real-Time Systems in a Platform-Independent Way

Jozef Hooman and Onno van Roosmalen

Appeared in: Parallel and Distributed Computing Practices, Volume 1, Number 2, pages 15-30, 1998.


To design distributed real-time systems, we distinguish two activities: (1) a platform-independent programming activity and (2) the realization of the resulting program on a particular execution platform. This paper concentrates on the first activity, proposing an extension of conventional (non-real-time) programming languages with so called timing annotations that specify the required timing constraints on an abstract level. A formal, axiomatic, semantics of a simple programming language with timing annotations is formulated, using specifications that are based on pre- and postconditions. Program correctness is independent of any underlying execution platform and can be proved by means of compositional proof rules. This is illustrated by a small example of a control system.