Validating Real Time Specifications using Real Time Event Queue Modeling

Interrupt-driven real time control software is difficult to design and validate. It does not line up well with traditional state-based, timed-transition specification formalisms, due to the complexity of timers and the pending interrupt queue. The present work takes a new approach to the problem of modeling and tool-supported reasoning about such systems based on infinite-state modeling of the temporal event queue. This approach, RTEQ, can be used in any formalism or tool set supporting function rich modeling. The present paper describes the approach, explores its expressive power and semantics, and describes a significant industrial case study applying it to the design of a novel network medium access controller for wireless communications.