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.