Abstract
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 language | English |
|---|---|
| Pages (from-to) | 520-551 |
| Number of pages | 32 |
| Journal | Formal Methods in System Design |
| Volume | 43 |
| Issue number | 3 |
| Early online date | 24 Aug 2013 |
| DOIs | |
| Publication status | Published - Dec 2013 |
Keywords
- Circus
- Complex real-time systems
- Time bands
- UTP