|
SafeDpi is a distributed version of the picalculus, in which processes
are located at dynamically created sites.
Parametrised code may be sent between sites using so-called
ports, which are essentially higher-order versions of
picalculus communication channels. A host location may protect itself
by only accepting code which conforms to a given type associated to
the incoming port.
We define a sophisticated static type system for these ports, which
restrict the capabilities and access rights of any processes launched
by incoming code. Dependent and existential types are used to add
flexibility, allowing the behaviour of these launched processes,
encoded as process types, to depend on the host's instantiation
of the incoming code.
We also show that a natural contextually defined behavioural
equivalence can be characterised coinductively, using bisimulations
based on typed actions. The characterisation is based on the
idea of knowledge acquisition by a testing environment and makes
explicit some of the subtleties of determining equivalence in this
language of highly constrained distributed code.
|
