Formal Platform-Independent Design of Real-Time Systems
A. Sintotski, D.K. Hammer, O. van Roosmalen, and
J. Hooman
Appeared in: Proceedings 13th Euromicro Conference on Real-Time Systems,
IEEE Computer Society Press, pages 163 - 170, 2001.
ABSTRACT
A formal approach for the development of real-time control systems is described.
Our development process consists of two phases: the platform-independent phase,
which includes specification, programming, and verification, and the second
phase, where execution platform considerations (i.e. resource constraints) are
taken into account. This development process supports the use of end-to-end
timing constraints through the whole design process without splitting them
apart. A real-time application is modeled as a parallel composition of objects
communicating by means of asynchronous message passing. This work concentrates
on a compositional framework that combines the specification and verification
of functional requirements and end-to-end timing constraints into one consistent
formal model. In this paper we apply the approach to the mine pump control
system. The formal analysis shows that a previously published
implementation of the mine pump control system is incorrect.
A extended version of this work appeared as
D.K. Hammer, J. Hooman, M.A. Reniers, O. van Roosmalen, A. Sintotski,
Design of the mine pump control system,
Computing Science Reports 01/05, Eindhoven University of Technology,
p. 70, 2001.