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

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 executable platform. This paper concentrates on the first
activity, proposing an extension of conventional(non-real) 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
post conditions. 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.