1Schedulability and Compatibility of Real Time Asynchronous Objects

Abstract—We apply automata theory to specifying behavioral inter-faces of objects and show how to check schedulability and compatibility of real time asynchronous objects. The behavioral interfaces of real time objects specify (the order and timings of) the messages an object may send and receive. Each object is checked against its behavioral interface; first, to guarantee its correct output behavior, and second to make sure that every message it may receive is processed within the designated deadline (schedulability analysis). Next, we propose a new technique for testing whether every object is used as expected (i.e., according to its behavioral interface) when combined with other objects (compatibility check). Compatibility additionally implies schedulability in the context of the actual system. The analyses are automated using the UPPAAL model checker. Our method makes it possible to put a finite bound on the message queue and still obtain schedulability results that are correct for any queue length.