University of Limerick Institutional Repository

Browsing Centres Science and Engineering by Author "Butterfield, Andrew"

DSpace/Manakin Repository

Browsing Centres Science and Engineering by Author "Butterfield, Andrew"

Sort by: Order: Results:

  • Butterfield, Andrew; Ó Catháin, Art (Springer, 2009)
    We present a CSP model of the internal behaviour of Flash Memory, based on its speci cation by the Open Nand-Flash Interface (ONFi) consortium. This contributes directly to the low-level modelling of the data-storage ...
  • Gancarski, Pawel; Butterfield, Andrew (Springer, 2009)
    This paper describes a complete denotational semantics, in the UTP framework, of slotted-Circus, a generic framework for reasoning about discrete timed/synchronously clocked systems. The key result presented here is a ...
  • Beg, Arshad; Butterfield, Andrew (2010)
    Following the development of formalisms based on data and behavioural aspects of the system, there are number of attempts in which these two formalisms are mixed together to get benefit of both paradigms. 'Circus' being a ...
  • Butterfield, Andrew; Freitas, Leo; Woodcock, Jim (Elsevier, 2007)
    We present second steps in the construction of formal models of NAND flash memory, based on a recently emerged open standard for such devices. The model is intended as a key part of a pilot project to develop a verified ...
  • Beg, Arshad; Butterfield, Andrew (2010)
    We present our experience of working with the Failures-Divergence Refinement (FDR) toolkit while extending our modelling of the behaviour of Flash Memory. This effort is a step towards the low-level modelling of data-storage ...
  • Gancarski, Pawel; Butterfield, Andrew (Springer-Verlag, 2010)
    This paper describes an extension adding priority to slotted-Circus, a generic framework for reasoning about discretely timed and/or synchronously clocked systems. The semantics of prioritised external choice is given using ...
  • Butterfield, Andrew (Springer-Verlag, 2010)
    Saoithin is a theorem prover developed to support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support the higher-order logic, alphabets, equational reasoning and "programs as ...

Search DSpace


Advanced Search

Browse

My Account