SAFEDPI: A language for controlling mobile code
Citation:
Hennessy, M., Rathke, J., Yoshida, N. , SAFEDPI: A language for controlling mobile code , Acta Informatica, 42, 4-5, 2005, 227-290Download Item:
Abstract:
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 de ne 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
exibility,
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 de ned 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.
Sponsor
Grant Number
Engineering and Physical Sciences Research Council (EPSRC)
GR/T04724/01
Engineering and Physical Sciences Research Council (EPSRC)
GR/T03208/01
Engineering and Physical Sciences Research Council (EPSRC)
GR/S55538/01
Author's Homepage:
http://people.tcd.ie/mcbhenneDescription:
PUBLISHED
Author: HENNESSY, MATTHEW
Type of material:
Journal ArticleSeries/Report no:
Acta Informatica;42;
4-5;
Availability:
Full text availableMetadata
Show full item recordLicences: