Proof methodologies for behavioural equivalence in DPI
Item Type:Book Chapter
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 Rathke
proof.pdf (Published (author's copy) - Peer Reviewed) 144.6Kb
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: HENNESSY, MATTHEW
Type of material:Book Chapter
Availability:Full text available