Slotted-Circus: A UTP-Family of Reactive Theories
Item Type:Conference Paper
Citation:Andrew Butterfield, Adnan Sherif and Jim Woodcock, Slotted-Circus: A UTP-Family of Reactive Theories, Lecture Notes in Computer Science, Integrating Formal Methods 2007 (IFM2007), Oxford, UK, 2-5 July, J. Davies and J. Gibbons, 4591, Springer, 2007, 75-97
Slotted-Circus - A UTP-Family of Reactive Theories.pdf (Published (author's copy) - Peer Reviewed) 284.4Kb
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.
Author: BUTTERFIELD, ANDREW
Type of material:Conference Paper
Availability:Full text available