University of Limerick Institutional Repository

Browsing by Author "Butterfield, Andrew"

DSpace Repository

Browsing 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 ...
  • Bresciani, Riccardo; Butterfield, Andrew (IEEE Computer Society, 2009)
    When some agents want to communicate through a media stream (for example voice or video), the Real Time Protocol (RTP) is used. This protocol does not provide encryption, so it is necessary to use Secure RTP (SRTP) to ...
  • Bresciani, Riccardo; Butterfield, Andrew (Springer, 2013)
    We have introduced probability in the UTP framework by using functions from the state space to real numbers, which we term distributions, that are embedded in the predicates describing the di er- ent program constructs. ...
  • 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 (2012)
    U (TP)2 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 ...
  • 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 ...
  • Bresciani, Riccardo; Butterfield, Andrew (2012)
    We present a theory of designs based on functions from the state space to real numbers, which we term distributions. This theory uses predicates, in the style of UTP, based on homogeneous relations between distributions, ...
  • 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 ...
  • Butterfield, Andrew; Sanán, David; Hinchey, Mike (2013)
    The best approach to verifying an IMA separation kernel is to use a (fixed) time-space partitioning kernel with a multiple independent levels of separation (MILS) architecture. We describe an activity that explores the ...
  • Bresciani, Riccardo; Butterfield, Andrew (Springer, 2012)
    We present an encoding of the semantics of the probabilis- tic guarded command language (pGCL) in the Unifying Theories of Programming (UTP) framework. Our contribution is a UTP encoding that captures pGCL programs as ...
  • Bresciani, Riccardo; Butterfield, Andrew (Association for Computing Machinery, 2009)
    The Dolev-Yao model has been widely used in protocol verificaion and has been implemented in many protocol verifiers. There are strong assumptions underlying this model, such as perfect cryptography: the aim of the ...

Search DSpace

Browse

My Account

Statistics