A Timed Model of Circus with the Reactive Design Miracle
2010
We propose a timed model of Circus which is a compact extension of original Circus. Apart from introducing time, this model uses UTP-style semantics to describe each process as a reactive design. One of significant contributions of our timed model is to extensively explore the reactive design miracle, the top element of a complete lattice with respect to the implication ordering. The employment of the miracle brings a number of brand-new features such as deadline and urgent events, which provide a more powerful and flexible expressiveness in system specifications.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
29
References
8
Citations
NaN
KQI