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.