Slotted-Circus: A UTP-Family of Reactive Theories
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-97Download Item:
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.
Author's Homepage:
http://people.tcd.ie/butrfeldDescription:
PUBLISHEDOxford, UK
Author: Butterfield, Andrew
Other Titles:
Lecture Notes in Computer ScienceIntegrating Formal Methods 2007 (IFM2007)
Publisher:
SpringerType of material:
Conference PaperCollections
Series/Report no:
4591Availability:
Full text availableKeywords:
Computer ScienceSubject (TCD):
Smart & Sustainable PlanetDOI:
http://dx.doi.org/10.1007/978-3-540-73210-5_5Metadata
Show full item recordLicences: