Modelling temporal behaviour in complex systems with Timebands

Kun Wei*, Jim Woodcock, Alan Burns

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review


Complex real-time systems exhibit dynamic behaviours on many different time levels. To cope with the wide range of time scales and produce more dependable computer-based systems, we develop a Timebands model that can explicitly recognise a finite set of distinct time bands in which temporal properties and associated behaviours are described. In order to formalise the Timebands model, we propose a new timed model, named Timed Circus, of Circus, which is the combination of Z, CSP, and the refinement calculus in the setting of Unifying Theories of Programming. Different from most approaches such as Timed CSP, Timed Circus uses a complete lattice in the implication ordering to model the distinctive features of the Timebands model. As a result, the semantics of the Timebands model is built upon Timed Circus to guarantee soundness of each operator and maintain consistency and coordination between different time bands. By means of two small systems, we demonstrate how the Timebands model contributes to describing complex real-time systems with multiple time scales.

Original languageEnglish
Pages (from-to)520-551
Number of pages32
JournalFormal Methods in System Design
Issue number3
Early online date24 Aug 2013
Publication statusPublished - Dec 2013


  • Circus
  • Complex real-time systems
  • Time bands
  • UTP

Cite this