## 4   Result

Our analyzer produces a html file containing a description of the input system behaviour.

### 4.1   Control flow

System control flow describes both the potential interactions between its own agents and the potential interactions between its agents and an hostile context. Due to the approximation, some of the discovered interactions may be ineffective. But the analyzer detects all the interactions. So if the analyzer do not detect an interaction between two components, there can be no interactions between them.

#### 4.1.1   What is an interaction

We call an interaction between a name restriction (# x) and a variable y the fact that a channel name created by an instance of the name restriction (# x) may be communicated to the variable y. If both the name restriction (# x) and the variable y belong to the analyzed system, it is called an internal interaction, while if either the name restriction or the variable belongs to the hostile context, it is called an external interaction.

For each interaction ((# x),y), we collect an approximation of the set I(x,y) of pair of words (idp,idc) such that a channel name created by the name restriction of an instance the marker of which is idc can be communicated to the variable of an instance the marker of which is idp. This approximation is given by both two grammars describing respectively the set of the first components of the elements of I(x,y) and the set of second components of the elements of I(x,y) and a relational approximation which calculates a set a affine constrains which are satisfied by the letter occurrence number of both element components of I(x,y).

#### 4.1.2   Internal interactions

Internal interactions can be obtained by clicking on a name restriction, and then on a variable.

#### 4.1.3   Extermal interactions

There are two kind of external interactions:
• the context may create a channel name, and send it to the system. Those interactions are obtained by first clicking on the motif (Intruder) and then by clicking on the chosen variable;
• the context may receive a name created by the system. Those interactions are obtained by clicking on the chosen name restriction and then by clicking on the word (Intruder).

### 4.2   Occurrence counting

Occurrence counting analysis captures an upper approximation of the number of simultaneous instances of agents. It is obtained by considering a configuration as a multi-set of syntactic agents, abstracting away which names have been communicated to variables. Then we abstract the set of the multi-set associated to the reachable configurations in a relational domain [6]. For the sake of the simplicity we only display non relational information about occurrence number of agents. For that purpose, we associate to each syntactic agent an interval which described the potential number of simultaneous syntactic copies of this agent.

The result of this analysis is displayed as follows:
• unreachable code is displayed in grey;
• agents which may occurs an unbounded number of time simultaneously are displayed in orange. Due to the approximation of the analysis, it is only a warning, we cannot conclude whether the number of simultaneous occurrences of this agent is effectively unbounded or whether the analysis is not accurate enough;
• the label of each syntactic agent is tagged with the interval which describes its occurrence number.