Name
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, a server and its clients, metaservers installing memory services, and address their correctness in a relatively simple manner. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11562436_25 | FORTE |
Keywords | Field | DocType |
bisimulations up-to,behavioural equivalence,tractable collection,resource access policy,capability type,memory service,witness bisimulations,auxiliary proof method,proof methodology,simple manner,model simple,computer science | Firewall (construction),Computer science,Correctness,Installation,Theoretical computer science,Witness,Equivalence (measure theory),Bisimulation,Access control,Formal methods,Distributed computing | Conference |
Volume | ISSN | ISBN |
3731 | 0302-9743 | 3-540-29189-X |
Citations | PageRank | References |
2 | 0.37 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alberto Ciaffaglione | 1 | 58 | 9.97 |
| Matthew Hennessy | 2 | 2358 | 341.12 |
| Julian Rathke | 3 | 2 | 0.37 |