Previous Contents Next

2   Syntax

2.1   Input File

Our tool takes as an input an ASCII file containing the description of a p-calculus system. This description shall be recognized by the following grammar:

P ::= (# x)P (name restriction)
    aP (action with a continuation)
    a (action without continuation)
    (P | ... | P) (Parallel composition)
    (P + ... + P) (Internal choice)
a ::= x![x1;...;xn] (output)
    y?[y1;...;yn] (input)
    *y?[y1;...;yn] (replication)

Name restriction, input and replication are the only name binders. This means that in (# x)P (resp. y?[y1;...;yn]P) (resp. *y?[y1;...;yn]P) occurrences of x (resp. y1,...,yn) (resp. y1,...,yn) in P are considered bound. All other name occurrences are considered free.

2.2   Operational semantics

Name restriction introduces a fresh name in an agent; parallel composition allows in concurrently computing several agents; internal choice denotes a non deterministic choice between several agents, only one agent will be computed while the others will be ignored, the choice is internal and does not depend on the other agents. As an action, an agent can send or receive a message which is a tuple of channel names. The result of a communication is given by using substitution. We use a lazy version of replication: a resource is an agent which syntacticly duplicates itself before receiving a message. Lazy replications enable to trace agent creation.

2.3   Unsafe names

The analyzed system may contain free names. Such names are supposed to be shared with an hostile context. No assumptions are made on them origin, This means that we do not assume that they are distinct. The hostile context is enable to use unsafe names to interact with the system. It can spoil the system by sending unsafe names via an unsafe name, and it can spy the system by receiving names via an unsafe names, this way it gets control over the names it has received.

Previous Contents Next