Document Type

Technical Report

Publication Date

2005-11-23

Filename

WUCSE-2005-54.pdf

DOI:

10.7936/K7ZK5F2Z

Technical Report Number

WUCSE-2005-54

Abstract

Middleware for distributed real-time embedded (DRE) systems has grown increasingly complex, to address functional and temporal requirements of diverse applications. While current approaches to modeling middleware have eased the task of assembling, deploying and configuring middleware and the applications that use it, a lower-level set of formal models is needed to uncover subtle timing and liveness hazards introduced by interference between and within distributed computations, particularly in the face of alternative middleware concurrency strategies. In this paper, we propose timed automata as a formal model of low-level middleware building blocks from which a variety different middleware configurations can be constructed. When combined with analysis techniques such as model checking, this formal model can help developers in verifying the correctness of various middleware configurations with respect to the timing and liveness constraints of each particular application.

Comments

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

Share

COinS