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.
ABSTRACT
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.
Postscript