Composing Real-Time Concurrent Objects Refinement, Compatibility and Schedulability

Abstract. Concurrent objects encapsulate a processor each and com-municate by asynchronous message passing; therefore, they can be com-posed to naturally model distributed and embedded systems. We model real-time concurrent objects using timed automata and provide each ob-ject with a context-specific scheduling policy. The envisioned usage and guaranteed deadlines of each object is specified in its behavioral interface, given also in timed automata. Furthermore, multiple objects can be com-posed only if they are compatible, i.e., if they respect the expected use patterns given in the behavioral interfaces of each other. In this paper, we define refinement of timed automata with inputs and outputs from a new perspective and we take account of deadlines in the refinement the-ory. Within this framework, we study composition and compatibility of real-time concurrent objects, and apply it in the context of compositional schedulability analysis of multiple-processor systems.