Abstract
We present a generic framework of UTP theories for describing systems whose behaviour is characterised by regular time-slots, compatible with the general structure of the Circus language [WC01a]. This "slotted- Circus" framework is parameterised by the particular way in which event histories are observable within a time-slot, and specifies what laws a desired parameterisation must obey in order for a satisfactory theory to emerge. Two key results of this work are: the need to be very careful in formulating the healthiness conditions, particularly R2; and the demonstration that synchronous theories like SCSP [Bar93] do not fit well with the way reactive systems are currently formulated in UTP and Circus. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Butterfield, A., Sherif, A., & Woodcock, J. (2007). Slotted-circus A UTP-family of reactive theories. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4591 LNCS, pp. 75–97). Springer Verlag. https://doi.org/10.1007/978-3-540-73210-5_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
