Eliminating Queues from RT UML Model Representations

摘要: This paper concerns analyzing UML based models of distributed real time systems involving multiple active agents. In order to avoid the time-penalties incurred by execution synchronous operation calls, it is typically recommended restrict inter-task communication event-based through unbounded FIFO buffers. means that such potentially have an infinite number states, making them out reach for analysis techniques intended finite-state systems. We present a symbolic technique systems, which can be tuned give finite, possibly inexact representation state-space. The central idea eliminate buffers completely, and represent their contents implicitly, effect on receiving agent. propose natural class protocols we call mode separated, this both finite exact. result has impact responsiveness predictability end-to-end latencies, as well protocol verification, enabling automatic verification methods applied.