Previous Contents Next

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:

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:
Previous Contents Next