Formal modeling and analysis of real-time resource-sharing protocols in Real-Time Maude

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-theart scheduling algorithm. This paper also shows how our general techniques can be instantiated to model and analyze the well known priority inheritance protocol.

• Type: Conference
• Year: 2008
• Where: IPPS
• Authors: Peter Csaba Ölveczky, Pavithra Prabhakar, Xue Liu
• Keywords: Checking Real-time Resource-sharing, Distributed And Parallel Computing, General Techniques, IPPS 2008, Unknown Subtle Bug