A Multi-Mode Real-Time Calculus

The Real-Time Calculus (RTC) framework proposed in [5, 16] and subsequently extended [17, 18] is targeted towards analyzing heterogeneous real-time systems that process var-ious types of streaming data. The main strength of RTC is a count-based abstraction, where arrival patterns of event streams are specified as constraints on the number of events that may arrive over any specified time interval. A collec-tion of such constraints for different interval lengths are cap-tured as functions which denote upper and lower bounds on the event arrival process. The service availability of compu-tational resources is also specified in a similar fashion. In this framework, algebraic techniques can be used to compute system properties in a compositional way. Typical properties that fall under this regime are the maximum delay suffered by an event stream and the buffer space required to store events waiting to be processed. The main drawback of RTC is that it cannot model state information in a natural way. For example, when a scheduling policy depends on the fill-level of a certain buffer or there is a shift from one type of data stream into another. We extend here RTC in a manner that en-ables state information to be easily captured while limiting the state-space explosion caused by fine grained state-based mod-els such as timed automata [2] and Event Count Automata [6]. Our model, called multi-mode RTC, specifies the arrival pro-cess of an event stream or the availability of a resource as fi-nite automata whose states are annotated with arrival/service functions. Our new framework combines the expressiveness of state based models with the algebraic and compositional fea-tures of the RTC formalism. In particular, system properties within a single mode can be analyzed using the RTC-based al-gebraic techniques and state-space exploration can be used to piece together the results obtained algebraically for the indi-vidual modes. We show how to determine typical system prop-erties with the focus on efficient approximate techniques and illustrate the advantages of multi-mode RTCs using two case studies. I