2005 | OriginalPaper | Buchkapitel
Proof Methodologies for Behavioural Equivalence in Dpi
verfasst von : Alberto Ciaffaglione, Matthew Hennessy, Julian Rathke
Erschienen in: Formal Techniques for Networked and Distributed Systems - FORTE 2005
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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, a server and its clients, metaservers installing memory services, and address their correctness in a relatively simple manner.