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_Evading"|} [T= RUN({|Pusher_enteredV."Pusher_Evading"|})
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
Lost = AnyOtherDeadline({|call_searchObject|},s)
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.

Analysis of model revision 0 (download)

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

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)

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)

The basic timed requirements all pass as expected.

TB)

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.

Analysis of model revision 1 (download)

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:

A)

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,
evadeCall,evadeRet,
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)

The basic timed requirements all pass as expected.

TB)

Same as in the original revision.

Analysis of model revision 2 (download)

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:

A)

TA)

TB)

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.

RoboSim model (download

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 RoboSim model is also available.

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.

The simulation code is available for download here.

Simulation from RoboSim

Below is a video of a run of an ArGoS simulation corresponding to the RoboSim model.

The simulation code is available for download here.