Document Type

Technical Report

Department

Computer Science and Engineering

Publication Date

2008-01-01

Filename

wucse-2008-12.pdf

Technical Report Number

WUCSE-2008-12

Abstract

Component-based software architectures enable reuse by separating application-specific concerns into modular components that are shielded from each other and from common concerns addressed by underlying services. Even so, concerns such as invocation rates, execution latencies, deadlines, and concurrency and scheduling semantics still cross-cut component boundaries in many real-time systems. Verification of these systems therefore must consider how composition of components relates to timing, resource utilization, and other properties. However, existing approaches only address a sub-set of the concerns that must be modeled in component-based distributed real-time systems, and a new more comprehensive approach is thus needed. To address that need, this paper offers three contributions to the state of the art in verification of component-based distributed real-time systems: (1) it introduces a formal model called real-time component automata that combines and extends interface automata and timed automata models; (2) it presents new component composition operations for single-threaded and cooperative multitasking forms of concurrency; and (3) it describes how the composed models can be combined with task locations, a scheduling model, and a communication delay model, to generate a combined representation of the application components and supporting services that can be verified by existing model checkers. These contributions are embodied in an open-source tool prototype called the Real-time Component Model Translator (RTCMT).

Comments

This research was supported in part by NSF grant CCF-0448562 titled "CAREER: Time and Event Based System Software Construction."Permanent URL: http://dx.doi.org/10.7936/K7NG4NVJ

Download

Share

COinS