Reactive Designs of Interrupts in Circus Time

摘要

The concept of interrupts is important in system specifications across both software and hardware. However, behaviours of interrupts are difficult to capture particularly in a timed environment because of its complexity. In this paper, the catastrophic interrupt adopted by the standard CSP models, the generic interrupt presented by Hoare in his original CSP book and the timed interrupt (time-driven) given in Timed CSP are considered in Circus Time. The contribution of the paper is a development of the reactive design semantics of these three interrupt operators in the UTP, a collection of verified laws, and a comprehensive discussion on the subtle difference between catastrophic and generic interrupts in applications.