Formal Design of
Real-Time Components on a Shared Data Space Architecture
Ulrich Hannemann and
Jozef Hooman
Proceedings of the Annual International
Computer Software and Applications Conference
(COMPSAC 2001),
IEEE Computer Society Press, pages 143 - 150, 2001.
ABSTRACT
We present a formal approach to the top-down design of
real-time components that communicate using a
shared data space.
The approach is compositional, that is, only the formal
specifications of the components are used to
reason about their combined behaviour.
Formal reasoning is supported by the interactive theorem
prover PVS.
Our shared data space model is based on the software
architecture SPLICE, that allows loosely-coupled
components.
Our formalism is illustrated by the top-down design
of a small flight-tracking-and-display system, which
contains an event-driven and a time-driven component.
Formal correctness is established, given suitable
assumptions about the environment of the system and
relations between timing parameters.
Postscript
An extended version of this work, including PVS files,
appeared as
Top-down Design of a Command-and-Control System with Timing
Assumptions
Ulrich Hannemann and Jozef Hooman
Technical Report CSI - R 0116,
Computing Science Institute,
University of Nijmegen.
Postscript