Examples

5 Examples

We now interpret the results obtained when analyzing some examples.

5.1 The token-ring

5.1.1 The ring of processes

A ring of processes can be generated by the following system:


((# make)(# mon)(# left0)
((*make?[left](# right)(mon![left,right]|make![right]))
|(*make?[left](mon![left,left0]))
|make![left0]))

Channel names created by name restrictions (# left0) and (# right) denote the processes of the ring. The first process is created by the restriction (# left0). An agent mon![v₁;v₂] denotes a connection between two processes. Then each time the first resource is replicated, a new process is created and linked to the previous process, which has been passed as an argument of the replication. The second resource replication closes the ring by linking the last created process with the first created process.

Analysis output can be consulted.

The analyzer discovers that in each instance of the agent mon![left,right], the variable left is either bound to a name created by an instance of the (# right) restriction or to a name created by the (# left0) restriction, and the variable right is always bound to a name created by an instance of the (# right) restriction. More specifically, in the case where the variable left is bound to a name created by an instance of the (# right) restriction, it discovers that:

the instance marker of mon![left,right] is on the form (1,6)(1,3)ⁿ⁺¹,
while the marker associated to the channel name communicated to the variable left is (1,6)(1,3)ⁿ,
and the marker associated to the channel name communicated to the variable right is (1,6)(1,3)ⁿ⁺¹.

It is enough to prove that each processes can only be linked to either the next one or to the first one.

5.1.2 The token-ring

We consider the following mobile system:


((# make)(# mon)(# left0)
((*make?[left](# right)(mon![left,right]|make![right]))
|(*make?[left](mon![left,left0]))
|make![left0]
|(*mon?[prev,next](*prev?[](# crit)(crit![] | (crit?[]next![]))))
|left0![]))

An additional resource spawns a resource for each process of the ring. Then a token is put in the ring of processes: the token is denoted by syntactic copies of the agents next![] and left0![]. The name of this agent describes the token location. When a token is available, the corresponding process can duplicate its resource, as a result the process enters its critical session. The critical session is exited when the two agents crit![] and crit?[] have interacted, the token is then passed to the next process.

Analysis output can be consulted.

The analyzer discovers that at most one instance of the agent crit![] can simultaneously occur. We can conclude that at most one process can be in its critical section in the same time. We shall notice that this information cannot be calculated without relational information about occurrence number of agents. For instance, if we have no relation about the occurrence number of syntactic copies of the agent next![] and the one of the agent left0![], we cannot prove that they cannot simultaneously occur.

5.1.3 A wrong token-ring

We consider the following mobile system:


((# mon)(# left0)
((*make?[left](# right)(mon![left,right]|make![right]))
|(*make?[left](mon![left,left0]))
|make![left0]
|(*mon?[prev,next](*prev?[](# crit)(crit![] | (crit?[]next![]))))
|left0![]))

In this mobile system, the channel name make is unsafe, as a consequence, an intruder may spy for names created by the instances of the name restriction (# right), and may use them to insert an arbitrary number of tokens in the ring.

Analysis output can be consulted.

Our analyzer warns that channel names created by the instance of the name restriction (# right) may escape. It also discovers no bound to the occurrence number of the syntactic agent crit![]. Due to the approximation we cannot conclude whether there is a bug in the mobile system or whether the analysis is not precise enough.

5.2 An ftp-server

5.2.1 A correct ftp-server

An ftp-server can be described by the following system:


((# make)(# server)(# port)
((*make?[](# address)(# request)
        (
         (*address?[]server![address,request]) 
        |
         address![]
        | 
         make![]
        ))
|
 (*server?[email,data](# deal)
        (
         port?[](deal![data] | deal?[rep] (email![rep] | port![]))
        + 
         email![]
        ))
| port![] 
| port![] 
| port![] 
| make![]))

The first resource creates repeatedly a new customer which send a query to a server. This query is composed by a query request and an address address. The customer sends its query again in case it receives a failure report denoted by the agent address![]. The second resource describes the server. When this one receives a query, it duplicates itself. Then, either it uses an available port and computes the query or it reports a failure to the client by spawning the agent address![]. Available ports are denoted by agents port![]. Data processing just consists in a communication between two agent of the server, many computational feature are abstracted away. Then the port is released, while the answer is resent to the client.

Analysis output can be consulted.

The analyzer proves that a channel name created by the restriction (# address) can only be communicated to the variable email, or to the variable address and that a channel name created by the restriction (# request) can only be communicated to the variable request, to the variable data or to the variable rep. More specifically, it discovers that each time an agent email![rep], the agent marker is on the form (1,16).(1,5)ⁿ.((2,4).(6,3).(2,12))^m.(2,4).(6,3); the variable email is linked to a channel name created by the restriction (# address) of the instance the marker of which was (1,16).(1,5)ⁿ; the variable rep is linked to a channel name created by the restriction (# request) of the instance the marker of which was (1,16).(1,5)ⁿ. This is enough to prove that both variables email and data have created by the same instance of the client resource and so the answer to a query can only be resent to the good client.

The analyzer also discovers that the number of simultaneous instances of the syntactic agent deal![data] (which denotes the number of simultaneous sessions of the server) is always less than three.

5.2.2 A wrong ftp-server

We now consider the following system:


((# make)(# server)(# port)(# deal)
(
 (*make?[](# address)(# request)
         (
          (*address?[]server![address,request]) 
         |
          address![]
         | 
          make![]
         ))
|
 (*server?[email,data]
         (
          port?[](port![] | deal![data] | deal?[rep](email![rep]))
         + 
          email![]
         ))
| port![] 
| port![] 
| port![] 
| make![]))

This mobile system does not correspond to the specification we have given, because the connection is released before that the session is finished and simultaneous sessions can interact with each others.

Analysis output can be consulted.

Our analyzer can prove neither the integrity of the server, nor the non-exhaustion of the resources. But we cannot conclude that there are bugs, because of the approximation.