Timed Automata Model for Component-Based Real-Time Systems

One of the key challenges in modern real-time embedded systems is safe composition of different software components. Formal verification techniques provide the means for design-time analysis of these systems. This paper introduces an approach based on timed automata for analysis of such component-based real-time embedded systems. The goal of our research is to provide a method for treating the schedulability problem of such systems on multi-core platforms. Since the components are developed, analyzed and tested independent of each other, the impact of one component on the others does not depend on its internal structure. Therefore, we reduce the problem of proving the schedulability of the composed system to proving the schedulability of each component on the resource partition allocated to it based on the interface of the component. The proposed verification method is demonstrated on a H.264 decoder case study.