Handover Protocol

This example, extracted from Robin Milner's Communicating and Mobile Systems: the pi-calculus,
simulates the interaction going on between cell phones, the stations that directly communicate to the
cell phones and the centrals that regulate which station is to be used for the communications. The
general idea is to represent cell phone mobility, considering the shifting connectivity to the stations.

Starting by the definition of the behavior of a cell phone, it consists in either talking and continuing
with the initial communication links or switching to new communication links, which represents a
change of the station used for communication.

defproc
    Mobile(talk,switch)=
        select {
            talk?().Mobile(talk, switch);
            switch?(talkn, switchn).Mobile(talkn,switchn)
        };

Now it is possible to define the station's behavior simply by saying that it can either communicate to the
cell phone or pass away the connectivity to another base station, by means of a communication with the
central, and become idle after which waiting for the next cell phone assignment coming from the central.

defproc
    BaseStation(talk, switch, give, alert) =
        select {
            talk!().BaseStation(talk, switch, give, alert); 
            give?(talkn, switchn).switch!(talkn,switchn).
                BaseStationIdle(talk,switch, give, alert)
        }
and
    BaseStationIdle(talk, switch, give, alert) = 
        alert?().BaseStation(talk, switch, give, alert);

Finally we have the central whose job is simply to inform a base station that it has to give the connectivity
to other station after which alerting this newly appointed station that it has to operate this connection,
alternating the roles of the stations in the next step.

defproc
    Central(talk, talkNxt,
            switch, switchNxt,
            give, giveNxt,
            alert, alertNxt) = 
        give!(talkNxt, switchNxt).alertNxt!().Central(talkNxt, talk,
                                                      switchNxt, switch,
                                                      giveNxt, give,
                                                      alertNxt, alert);

To finish off the process definitions a very simple system is defined having just one cell phone, the two
alternating base stations and a central.

defproc
    System = (new talk1, talk2,
                  switch1, switch2,
                  give1, give2,
                  alert1, alert2
                    in ( 
                        Mobile(talk1, switch1) |
                        BaseStation(talk1,switch1,give1,alert1) |
                        BaseStationIdle(talk2,switch2,give2,alert2) |
                        Central(talk1, talk2,
                                switch1, switch2,
                                give1, give2,
                                alert1, alert2)
                    ));

We now define a standard behavioral property that expresses that the system is never deadlocked, i.e.,
has a possible reduction in every possible configuration.

defprop deadLockFree = maxfix X. (<>true and []X);

And we check to see if the system satisfies this property.

check System |= deadLockFree;

We now intend to verify that our system is race free, or in other words, does not have two processes
trying to write on a channel while another one is trying to read on it. We start by saying that a writer
is a single point in space and is willing to do an output in a determined channel. Analogously for the
reader considering a read instead of a write.

defprop write(x) = (1 and < x! >true);

defprop read(x) = (1 and < x? >true);

We now state that the existence of a race can be specified by looking underneath all restrictions and
finding a channel name such that the system can be divided in three our more parts, being two of these
parts writers on that channel and a third part a reader that uses that channel.

defprop hasRace = 
    inside (exists x.(write(x) | write(x) | read(x) | true));

Finally we state that race freeness is not having a race in any possible configuration.

defprop raceFree = maxfix X.((not hasRace) and []X);

We check to see if our system satisfies this property.

check System |= raceFree;