Formal modeling and analysis of real-time resource-sharing protocols in Real-Time Maude
Peter Csaba Ölveczky, Pavithra Prabhakar, Xue Liu · Proceedings - IEEE International Parallel and Distributed Processing Symposium · 2008
This paper presents general techniques for formally modeling, simulating, and model checking real-time resource-sharing protocols in Real-Time Maude. The "scheduling subset" of our techniques has been used to find a previously unknown subtle bug in a state-of-the-art scheduling algorithm. This paper also shows how our general techniques can be instantiated to model and analyze the well known priority inheritance protocol.