Document Type

Technical Report

Department

Computer Science and Engineering

Publication Date

2008-01-01

Filename

wucse-2008-1.pdf

Technical Report Number

WUCSE-2008-1

Abstract

Component based middleware helps to facilitate software reuse by separating application-specific concerns into modular components that are shielded from the concerns of other components and from the common concerns addressed by underlying middleware services. In real-time systems, concerns such as invocation rates, execution latencies, deadlines, and concurrency semantics cross-cut multiple component and middleware abstractions. Thus, the verification of these systems must consider features of the application components (e.g., their execution latencies and relative invocation rates) and of the supporting middleware (e.g., concurrency and scheduling) together. However, existing approaches only address a sub-set of the features that must be modeled in component based real-time systems, and a new more comprehensive approach is needed. To address that need, this paper offers three main contributions to the state of the art in the verification of component based real-time systems: (1) it introduces a formal model called component automata that combines new input/output rate specifications with input/output actions and timed internal actions from the existing interface automata and timed automata models respectively; (2) it presents new component composition operations for single-threaded and cooperative multi-tasking, in addition to composition under the preemptive multi-tasking semantics assumed by interface automata; and (3) it describes how the composed component models then can be combined with task location specifications, a scheduling model, and a communication delay model, to generate a combined timed automaton representation of the components and middleware that can be verified by existing timed model checkers. This research was supported in part by NSF grant CCF-0448562 titled CAREER: Time and Event Based System Software Construction.

Comments

Permanent URL: http://dx.doi.org/10.7936/K7S75DJT

Download

Share

COinS