Modelling and Implementing Complex Systems with Timebands

We describe how to use a timeband 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. Our models are written using CSP and checked using the FDR model checker. More complicated models use Circus, the state-rich process algebra. We show how to implement such a timeband architecture using the JCSP Java class library.