Formal Reasoning about Real-time Components on a Data-oriented Architecture

Ulrich Hannemann and Jozef Hooman

Proceedings of 6th World Multiconference on Systemics, Cybernetics and Informatics (SCI02), 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 its use with an example of a flight-tracking-and-display system.