# Transport

## Introduction

This report documents the development of a model of a single robot in the context of an occlusion-based transport swarm. The original application is described in “A Strategy for Transporting Tall Objects within a Swarm of Miniature Mobile Robots”.

## Module

The module `System`, including the robotic platform `ePuck`, the controller `Controller` and the reference to the state-machine `Pusher` are reproduced below. In addition we also show the operations used by the state-machine `Pusher`, which we specify as terminating.

The robotic platform can raise any of the following events:

• `objectSeen.d`: in response to an object being detected, with parameter `d` containing an estimate of the distance to the object.
• `goalSeen`: in response to seeing the goal.
• `neighbourDetected.n`: in response to detecting `n` neighbours in the vicinity.

## State-machine

The state-machine `Pusher` is reproduced below, and described in what follows.

In state `Searching` the robot searches for an object by calling `searchObject` and, once it sees one, it transitions to state `MovingToObject` as triggered by the event `objectSeen`, which receives and assigns the estimated distance to variable `distance`. If the object is nearby, so the condition `distance<close` holds, then the state-machine can transition to state `ClosingInOnObject`. While in states `MovingToObject` and `ClosingInOnObject` if the object is lost for a certain amount of time `Ta`, then the robot initiates another search for the object by transitioning to state `Searching`.

When the robot is close enough to the object, satisfying condition `distance == 0`, then it transitions from state `ClosingInOnObject` to `Scanning` and disables the object tracking facility by calling `disableObjectWatch`. In state `Scanning` the robot initializes the variable `goal` to `false`, assuming that the goal is not visible until the first time event `goalSeen` takes place, and enables the capability to find the goal by calling `enableGoalFinding`.

Once the state `Scanning` has been entered, `scanAndAlign` is called, so that the robot can perform an alignment procedure, and a decision is taken two either transition to `MovingAround` if the goal is seen, or to transition to `Pushing` if the goal is not seen. When taking this transition we initialize the variable `neighbours`, which keeps track of the number of nearby neighbours, to `2`. This prevents the transition from `Pushing` to `Scanning` from being triggered unless `Tb` time units have passed since the most recent time, after having entered `Pushing`, where the number of neighbours was observed to drop below `2`, which can only be appropriately checked once at least one reading of `neighbourDetected` has occurred. In state `Pushing` the robot first calls `enabledObjectWatch` to enable the facility to track the object, followed by the call to `enableNeighbourDetection` to enable the facility to track neighbours. Once state `Pushing` is entered it finally calls the operation `pushObejct` and can receive events `objectSeen` and `neighbourDetected`.

The transition from `Pushing` to `Evading` takes place whenever the object has been lost for at least `Tc` time units. We specify this behaviour by taking into account the `distance` to the object as given by `objectSeen` together with clock `C`. Whenever the `distance` changes to being greater than `0`, we reset clock `C`. The four possible cases are treated by separate transitions whose guards are summarized below:

• `objectSeen?d[distance==0/\d==0]`: the object is seen at distance `0`, so there is no need to change the existing value of `distance`.
• `objectSeen?d[distance==0/\d>0]/#C;distance=d`: if the object was previously at distance `0`, and is now at a distance greater than `0`, then clock `C` is reset and the new value `d` assigned to `distance`. Here we capture the change
• `objectSeen?d[distance>0/\d==0]/distance=d`: if the current distance is greater than `0`, and the new distance is `0`, then we just record the new value `d` in `distance`.
• `objectSeen?d[distance>0/\d>0]`: in every other case, we do not update the value of `distance`.

The transition from `Pushing` to `Scanning` takes place whenever less than `2` `neighbours` have been observed for at least `Tb` time units. We specify this behaviour using the variable `neighbours` together with clock `N`, so that whenever the value drops below `2` we count the time using clock `N`. We specify this using four transitions, whose guards are summarized below:

• `neighbourDetected?n[neighbours<2/\n<2]`: the current count of `neighbours` is less than `2` and the new value being communicated is also less than `2`, so there is no need to record a change.
• `neighbourDetected?n[neighbours>=2/\n<2]/#N;neighbours=n`: the current count of `neighbours` is greater than or equal to `2`, and the new value is less than `2`, in which case we have a change to a situation of less than `2` neighbours, so we reset clock `N` and assign the new value `n` to `neighbours`.
• `neighbourDetected?n[neighbours<2/\n>=2]/neighbours=n`: the current count of `neighbours` is less than `2` and the new value `n` is greater than or equal to `2`, so there is a change to a situation in which at least `2` neighbours are around, so we updated the value of `neighbours` to `n`.
• `neighbourDetected?n[neighbours>=2/\n>=2]`: in every other case in which the count of current `neighbours` or the new value `n` is above `2` we do not update the variable `neighbours`.

Before exiting state `Pushing` the capability to track the object and the neighbours is disabled by calling `disableObjectWatch` and `disableNeighbourDetection`, respectively.

In general, the value of a `since(C)` condition for a clock `C` that has not been reset is arbitrary. We observe that in the case of the guard `distance>0/\since(C)>=Tc`, `since(C)>=Tc` has an appropriate value when `distance>0` is `true` because clock `C` is reset precisely when the value of `distance` becomes greater than `0`. Similarly in the case of the guard `neighbours<2/\since(N)>=Tb`, `since(N)>=Tb` has an appropriate value when `neighbours<2` is `true` because clock `N` is reset precisely when the number of `neighbours` goes below `2` as explained above.

In state `Evading` the robot evades the vicinity by calling the operation `evade`. After exactly `Te` time units it transitions to state `Searching`. Similarly, in state `MovingAround` the robot calls `moveAroundObject` which takes the robot around the object. After exactly `Td` time units it transitions to state `Searching`.

We observe that the state-machine, and indeed the robotic controller, never terminates. This follows closely the description of the algorithm in the original paper. However in the reported trials, robots could be stopped by a central controller that can ascertain whether the object has been made contact with the goal, or after a certain amount of time. We do not model that facility in this model.

## Requirements

As a basis for verification, we define a few requirements for the transport controller, called `Pusher`, and encode them as suitable CSP assertions.

### A) Basic Requirements

The timed `tock-CSP` process is `T_System`.

#### 1) System behaviour is deterministic.

`assert T_System :[deterministic]`

#### 2) System behaviour is divergence free.

`assert T_System :[divergence free]`

### TA) Basic Timed Requirements

We identify the visible behaviours which the environment can delay arbitrarily by defining the set `System_ExternalEvents`:

``````System_ExternalEvents = {|goalSeen,neighbourDetected,objectSeen|}
``````

#### 1) Pusher is timelock free.

``````assert RUN({tock}) ||| CHAOS(System_ExternalEvents) [F= T_Pusher |\ union(System_ExternalEvents,{tock})
``````

#### 2) Every state is reachable.

Since here we are interested in observing states being entered, we use `T_System_VS` a version of `T_System`, which allows the events `Pusher_enterV`, `Pusher_enteredV`, `Pusher_exitV` to be observed.

``````assert not STOP [T= T_System_VS |\ {|Pusher_enteredV."Pusher_Searching"|}
assert not STOP [T= T_System_VS |\ {|Pusher_enteredV."Pusher_MovingToObject"|}
assert not STOP [T= T_System_VS |\ {|Pusher_enteredV."Pusher_MovingToObject_Watch"|}
assert not STOP [T= T_System_VS |\ {|Pusher_enteredV."Pusher_ClosingInOnObject"|}
assert not STOP [T= T_System_VS |\ {|Pusher_enteredV."Pusher_ClosingInOnObject_Watch"|}
assert not STOP [T= T_System_VS |\ {|Pusher_enteredV."Pusher_Scanning"|}
assert not STOP [T= T_System_VS |\ {|Pusher_enteredV."Pusher_Scanning_Watch"|}
assert not STOP [T= T_System_VS |\ {|Pusher_enteredV."Pusher_Pushing"|}
assert not STOP [T= T_System_VS |\ {|Pusher_enteredV."Pusher_Pushing_Watch"|}
assert not STOP [T= T_System_VS |\ {|Pusher_enteredV."Pusher_Evading"|}
assert not STOP [T= T_System_VS |\ {|Pusher_enteredV."Pusher_MovingAround"|}
``````

#### 3) The system cannot engage in an infinite number of internal events over a finite time interval.

``````assert T_System |\ union(System_ExternalEvents,{tock}) :[divergence free]
``````

#### 4) States can be visited inifitely often.

``````assert T_System_VS |\ {|Pusher_enteredV."Pusher_Searching"|} [T= RUN({|Pusher_enteredV."Pusher_Searching"|})
assert T_System_VS |\ {|Pusher_enteredV."Pusher_MovingToObject"|} [T= RUN({|Pusher_enteredV."Pusher_MovingToObject"|})
assert T_System_VS |\ {|Pusher_enteredV."Pusher_MovingToObject_Watch"|} [T= RUN({|Pusher_enteredV."Pusher_MovingToObject_Watch"|})
assert T_System_VS |\ {|Pusher_enteredV."Pusher_ClosingInOnObject"|} [T= RUN({|Pusher_enteredV."Pusher_ClosingInOnObject"|})
assert T_System_VS |\ {|Pusher_enteredV."Pusher_ClosingInOnObject_Watch"|} [T= RUN({|Pusher_enteredV."Pusher_ClosingInOnObject_Watch"|})
assert T_System_VS |\ {|Pusher_enteredV."Pusher_Scanning"|} [T= RUN({|Pusher_enteredV."Pusher_Scanning"|})
assert T_System_VS |\ {|Pusher_enteredV."Pusher_Scanning_Watch"|} [T= RUN({|Pusher_enteredV."Pusher_Scanning_Watch"|})
assert T_System_VS |\ {|Pusher_enteredV."Pusher_Pushing"|} [T= RUN({|Pusher_enteredV."Pusher_Pushing"|})
assert T_System_VS |\ {|Pusher_enteredV."Pusher_Pushing_Watch"|} [T= RUN({|Pusher_enteredV."Pusher_Pushing_Watch"|})
assert T_System_VS |\ {|Pusher_enteredV."Pusher_MovingAround"|} [T= RUN({|Pusher_enteredV."Pusher_MovingAround"|})
``````

### TB) Model Timed Requirements

Here we specify some timed requirements that the state-machine should satisfy.

#### 1) Provided `goalSeen` happens no more often than every `g` time units then at least `t` time units is spent in the state `Scanning` of the state-machine `Pusher`.

To specify this property we first define a process `StateSpent(S,t)` that requires `t` time units to be spent in state `S`.

``````StateSpent(S,t) =
let
Main = AnyOther({|Pusher_enteredV.S|}) ; TimedInterrupt(CHAOS(diff(Events,{|Pusher_exitV.S|})),t) ; AnyOther({|Pusher_exitV.S|}) ; Main
within
timed_priority(Main)
``````

It is defined by initially offering every event nondeterministically (specified using the process `AnyOther(x)` that offers every event nondeterministically and then terminates once the event `Pusher_enteredV.S` is performed). Then a timed interrupt offers every event other than `Pusher_exitV.S` nondeterministically, and after `t` time units offers every event nondeterministically also using `AnyOther(x)`, such that once `Pusher_exitV.S` is performed the process terminates and then behaves as `StateSpent(S,t)`.

To capture the property that the environment does not allow `goalSeen` to occurr more often than every `g` time units we define the following process `goalSeenEvery(g)`.

``````goalSeenEvery(g) = EDeadline(goalSeen,0) ; WAIT(g) ; goalSeenEvery(g)
``````

It initially requires the event `goalSeen` to take place immediately followed by a period `g` after which it recurses.

We can then check that the system satisfies our requirement by requiring that the process `T_System_VS` (which models the system and makes visible the events `Pusher_enteredV` and `Pusher_exitV`) composed in parallel with our assumption about the environment, as modelled by `goalSeenEvery(g)`, is a refinement of `StateSpent("Pusher_Scanning")`. Essentially the parallel composition allows us to restrict the possible behaviour of the environment.

``````assert StateSpent("Pusher_Scanning",t) [FD= timed_priority(T_System_VS [| { goalSeen } |] goalSeenEvery(g))
``````

#### 2) Whenever the system loses track of the object for more than `Ta` time units, then the robot resumes the search within `s` time units.

We encode this requirement through the following CSP process `LostTrackToSearch(s)` which is parametrised by `s`. First it offers any event nondeterministically, and once `objectSeen` happens then it behaves as `ObjectDetected` unless the internal event `lost` (declared for the purpose of defining this process) is observed, after which it behaves as `Lost`. The process `ObjectDetected` offers any event other than `lost` nondeterministically for a time `Ta`, after which the event `lost` can happen, unless the `objectSeen` event was observed, and so it recurses. Finally the process `Lost` requires the call of operation `searchObject` to take place within `s` units.

``````LostTrackToSearch(s) =
let
Init = AnyOther({|objectSeen|}) ; (ObjectDetected [| {lost} |> Lost) \ {lost}
ObjectDetected = TimedInterrupt(CHAOS(diff(Events,{lost})),Pusher_Ta) ; lost -> SKIP [| {|objectSeen|} |> ObjectDetected
within
timed_priority(Init)
``````

In this case we are interested in `s` being `0`, that is, once it has not seen an object more recently than `Ta` then immediately is starts searching again.

``````assert LostTrackToSearch(s) [FD= T_System
``````

# Analysis

Below we discuss the results of our analysis of the requirements.

For the purpose of our analysis we consider the following parameter settings:

Parameter Setting
Ta 1
close 1
Tb 1
Tc 1
Td 1
Te 1

We observe that in the automatically generated model, and since the variables are parameters of the state-machine `Pusher`, their names are prefixed with `Pusher_`, so that, for example, variable `Ta` is actually named as `Pusher_Ta`.

The initial value of `distance`, `newD` and `newN` are set to `0`. This is not relevant to the analysis as the conditions involving these variables succeed assignments to the respective variables. For example, `distance` is only compared after a communication through `objectSeen`. Similar case applies to the usage of `newD` and `newN`.

### A)

Requirement Result
A.1 fail
A.2 pass

The state machine is not deterministic as there are transitions guarded by time that compete nondeterministically. For example, the transition from state `MovingToObject` to state `ClosingOnObject`, when enabled competes with the self transition from state `Watch` inside state `MovingToObject`. To eliminate this nondeterminism, competing transitions need to have a negated timed constraint, so that whenever a transition with no trigger, but constrained by time is enabled, no other transitions are enabled.

### TA)

Requirement Result
TA.1 pass
TA.2 pass
TA.3 pass
TA.4 pass

The basic timed requirements all pass as expected.

### TB)

Requirement Result
TB.1 fail
TB.2 pass

The first requirement `TB.1` fails as the state `Scanning` can be interrupted without consuming any time. To eliminate this behaviour, while still allowing the during action to be executed (and possibly any behaviours inside the composite state), the transitions outgoing from `Scanning` need to have a conjunction with `sinceEntry(Scanning) > S`, where `S` defines a minimum execution time for the state `Scanning`.

To start addressing the nondeterministic behaviour of model above, we consider each transition guarded by a timed condition, and for every transition with the same source state (or contained within the same composite state) we add a corresponding negated condition as a conjunct. For example, we add the condition `since(T) < Ta` to the self-transition on state `Watch` inside state `MovingToObject`. In this way, that transition does not compete with the outgoing timed transition from `MovingToObject` to `Searching`. The resulting state machine is shown below.

For the purpose of our analysis we consider the following parameter settings:

Parameter Setting
Ta 1
close 1
Tb 1
Tc 1
Td 1
Te 1

### A)

Requirement Result
A.1 fail
A.2 pass

Analysis of requirement `A.1` reveals another counter-example for determinism:

``````First Behaviour: enableObjectWatchCall, enableObjectWatchRet, objectSeen.0
Acceptance set: {|enableGoalFindingCall|}

Second Behaviour: enableObjectWatchCall, enableObjectWatchRet, objectSeen.0
Acceptance set: moveToObjectCall
``````

This reveals that the call of operation `moveToObject` is not guaranteed to happen, because the transition from state `MovingToObject` to `ClosingInOnObject`, and subsequently to state `Scanning` is available following an `objectSeen.0` event (where `0 < close`), thus the state-machine could be in states `MovingToObject`, `ClosingInOnObject` or `Scanning`, following which it would call `enableGoalFinding` as shown in the counter-example.

Because we do not specify the operations `searchObject`, `moveToObject`, `closeInOnObject`, `evade`, `moveAroundObject`, `scanAndAlign`, and `pushObject`, nor do we specify deadlines on these, it is impossible to guarantee their deterministic execution, unless they are called as part of the entry action of each state. However, this is in general undesirable as we do not constrain their implementation.

Instead, we can consider whether the remainder of the state-machine’s behaviour is deterministic while ignoring the calls to the unspecified operations used in the during actions. We can proceed by defining the following process `T_System_NoDuring`, where we hide every operation call that is not of interest:

``````T_System_NoDuring = timed_priority(T_System \ {|moveToObjectCall,moveToObjectRet,
searchObjectCall,searchObjectRet,
closeInOnObjectCall,closeInOnObjectRet,
scanAndAlignCall,scanAndAlignRet,
moveAroundObjectCall,moveAroundObjectRet,
pushObjectCall,pushObjectRet|})
``````

The analysis of `A.1` considering `T_System_NoDuring` still reveals a counter-example for nondeterminism:

``````First Behaviour: enableObjectWatchCall, enableObjectWatchRet, disableObjectWatchCall, disableObjectWatchRet, enableGoalFindingCall, enableGoalFindingRet
Acceptance set: {|disableGoalFindingCall|}

Second Behaviour: enableObjectWatchCall, enableObjectWatchRet, disableObjectWatchCall, disableObjectWatchRet, enableGoalFindingCall, enableGoalFindingRet
Acceptance set: {|goalSeen|}
``````

The operation `disableGoalFinding` is called within the exit action of state `Scanning`. This counter-example shows that the state machine could nondeterministically perform the self-transition on state `Watch` within the composite state `Scanning` following a `goalSeen` event, or, could transition out of state `Scanning` to state `Pushing` and so calling the operation `disableGoalFinding` nondeterministically. In other words, it is not necessarily the case that the state-machine will be able to treat the event `goalSeen` in this situation.

To prevent the transition on `goalSeen` from being nondeterministic we could add a condition on that transition to mutually excluviely offer `goalSeen` or the transitions from `Scanning` to `MovingAround` and `Pushing`. Similarly if we kept on analysing the transitions in state `Pushing` we would also find such nondeterminism arising from the contention with the transitions from `Pushing` to `Evading` and `Scanning`, and those inside the substate `Watch` of state `Pushing`.

While the additional restrictions could make the state machine fully deterministic, there is no be benefit in doing so. For example, the search for an object still takes place after the timed threshold `Ta` even if the state machine is nondeterministic. Therefore we accept that although initially the requirement for determinism seemed sensible, there is no significant impact on the satisfiability of other timed requirements.

### TA)

Requirement Result
TA.1 pass
TA.2 pass
TA.3 pass
TA.4 pass

The basic timed requirements all pass as expected.

### TB)

Requirement Result
TB.1 fail
TB.2 pass

Same as in the original revision.

To accommodate requirement `TB.2` we make the following changes to state-machine `Pusher`:

• The outgoing transitions from state `Scanning` are guarded with a condition `sinceEntry(Scanning) >= S`, where `S` is a period of time during which scanning takes place.

We reproduce below the diagram.

For the purpose of our analysis we consider the following parameter settings:

Parameter Setting
Ta 1
close 1
Tb 1
Tc 1
Td 1
Te 1
S 1

### A)

Requirement Result
A.1 fail
A.2 pass

### TA)

Requirement Result
TA.1 pass
TA.2 pass
TA.3 pass
TA.4 pass

### TB)

Requirement Result
TB.1 pass
TB.2 pass

# Simulation of model revision 2

In this section we describe the use of the RoboChart model, and a corresponding RoboSim model, to construct a simulation in ArGoS, where the individual controllers are in correspondence with that specified in the original RoboChart model.

The project file contains a manually generated semantics of the simulation for the Transporter example, as well as its correctness verification. The simulation was verified against the RoboChart model with assumptions `TA1`, `TA2` and `TA3`.

The file with the CSP models and verification assertions is: `src-gen/timed/module_assertions-withoptimisations.cps`

The interested reader can load this file in the FDR4 tool and check the assertions. The relevant assertions are:

• Absence of deadlock below indicates that the RoboChart model is schedulable.
``````assert PMConstrainedSpecA3 \ ExternalEvents_System; TSTOP :[deadlock free]
``````
• The assertion below ensures that the RoboSim model is a refinement of the RoboChart one with the assumptions.
``````assert PMConstrainedSpecA3 \ ExternalEvents_System [F= SimSpec
``````
• We checked for divergence freedom using separate assertions:
``````assert SimSpec :[divergence free]
assert PMConstrainedSpecA3 \ ExternalEvents_System :[divergence free]
``````

### Simulation from RoboChart

Below is a video of a run of an ArGoS simulation as generated automatically from RoboChart.