Proof methodologies for behavioural equivalence in DPI
Citation:
Proof methodologies for behavioural equivalence in DPI , Lecture Notes in Computer Science, Berlin, Heidelberg, Springer, 2005, 335-350 , Alberto Ciaffaglione, Matthew Hennessy and Julian RathkeDownload Item:
Abstract:
We focus on techniques for proving behavioural equivalence between systems in Dpi, a
distributed version of the picalculus in which processes may migrate between dynamically created
locations, and where resource access policies are implemented by means of capability types.
We devise a tractable collection of auxiliary proof methods, relying mainly on the use of bisimulations
up-to -reductions, which considerably relieve the burden of exhibiting witness bisimulations.
Using such methods we model simple distributed protocols, such as crossing a firewall, the
interaction between a server and its clients, metaservers installing memory services, and address their
correctness in a relatively simple manner.
Author's Homepage:
http://people.tcd.ie/mcbhenneDescription:
PUBLISHED
Author: HENNESSY, MATTHEW
Publisher:
SpringerType of material:
Book ChapterAvailability:
Full text availableKeywords:
Computer Science, metaserversMetadata
Show full item recordLicences: