Formal Reasoning about Real-time Components on a Data-oriented Architecture
Ulrich Hannemann and
Proceedings of 6th World Multiconference on Systemics, Cybernetics and
Volume XI, pages 313--318, 2002.
We investigate an approach towards formal reasoning about
component-based software architecture.
In this paper we develop specification
schemes for real-time applications which interact via the
data-oriented software architecture SPLICE.
Composition of these
applications requires not only knowledge about the component
specifications, but also information about key parameters of the
underlying communication mechanism.
We formulate a proof scheme for
the interaction of data-oriented components, and illustrate
with an example of a flight-tracking-and-display system.