Technical Report Number
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 conﬁguring 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 conﬁgurations 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 conﬁgurations with respect to the timing and liveness constraints of each particular application.
Subramonian, Venika; Gill, Christopher; Sanchez, Cesar; and Sipma, Henry B., "Composable Models for Timing and Liveness Analysis in Distributed Real-Time Embedded Systems Middleware" Report Number: WUCSE-2005-54 (2005). All Computer Science and Engineering Research.