Date Added: Apr 2010
The authors describe how to use a time-band architecture to model real-time requirements. The architecture separates requirements that use different time units, producing a family of models. Each model is characterised by its granularity and precision. These models are then linked using superposition, a kind of event refinement, and a loose synchronisation of their time units, with respect to their precision. Their models are written using CSP and checked using the FDR model checker. More complicated models use Circus, the state-rich process algebra. They show how to implement such a time-band architecture using the JCSP Java class library.