Rteq: modeling and validating infinite-state hard-real-time systems

Abstract

Complex, interrupt-driven hard real time control software is difficult to design and validate. It does not line up well with traditional state-based, timed-transition approaches to real time system specification, 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 event queue modeling. This paper briefly overviews the approach and its application to a novel wireless medium access controller