Exploration

Introduction

This report documents the development of a model for an exploration robot, specified in RoboChart and analysed using FDR. First, we describe the requirements, and their formal CSP encoding suitable for verification with FDR, and then discuss the verification results for several iterations of the model, culminating in a version that satisfies all requirements.

Requirements

R1: Once a command is received the robot stops.

This requirement is encoded in CSP as follows.

StopOp = StopCall -> StopRet -> SKIP

Timed(OneStep) {
R1 = CHAOS(Events) [| {|VCModule_cmd|} |> (StopOp ; TSTOP)

assert timed_priority(R1) [FD= System
}

Within a timed section, the process R1 encodes the requirement. Initially it behaves as CHAOS(Events), the process that nondeterministically can perform any event in the set Events (of all events in scope). It can be interrupted by the event VCModule_cmd to behave as StopOp ; TSTOP, the sequential composition of StopOp, the process that models the call to operation Stop, and TSTOP, the timed deadlock process. Observe that the call to operation Stop needs to be completed without time passing.

The requirement is verified by stating that the System process, that is the calculated timed semantics of the RoboChart model, is a refinement of R1, where timed_priority is a function that ensures R1 has the correct timed semantics of tock-CSP as required for verification.

R2: Once the charging station is found, then the robot flashes its LEDs and stops. A command can still be accepted afterwards.

This requirement is encoded in CSP as follows.

Timed(OneStep) {
R2 = CHAOS(Events)
     [| {|VCModule_found|} |>
     (VCModule_flash.out -> StopOp; VCModule_cmd.in -> StopOp; STOP)
}

assert timed_priority(R2) [FD= System

We have, within a timed section, the process R2 defined using a pattern similar to R1. Initially it behaves as CHAOS(Events) and can be interrupted by VCModule_found to behave as the process that offers VCModule_flash.out, where out indicates that this is an output form the software to the robotic platform, followed by a call to operation Stop, and then also offers to accept a command, via the event VCModule_cmd.in, where in indicates that this is an input to the software.

Observe that VCModule_flash.out and VCModule_cmd.in have no timed constraints associated, and can therefore happen at any time. The calls to the operation Stop, however, do not consume time, and thus are specified, just as before, outside the timed section.

R3: While no command is issued, the robot should avoid obstacles, or reverse, when an obstacle is detected. Odometer readings may occur internally.

This requirement is encoded in CSP as follows.

ReverseOp = ReverseCall -> ReverseRet -> SKIP

-- The following process models the 'ChangeDirection' operation, which can
-- call 'TurnRight' or 'TurnLeft'. The decision whether to call one or the
-- other is internal to the state machine.

ChangeDirectionOp = ChangeDirectionCall ->
            (TurnRightCall -> TurnRightRet -> SKIP
            |~|
            TurnLeftCall -> TurnLeftRet -> SKIP)
            ; ChangeDirectionRet -> SKIP

Timed(OneStep) {
R3 = CHAOS(Events)
     [| {|VCModule_obstacle.in.Loc_left, VCModule_obstacle.in.Loc_right|} |>
     ((ChangeDirectionOp |~| ReverseOp) ; R3)

R3System = timed_priority((System [| {|VCModule_cmd|} |] SKIP) \ {|VCModule_odometer|})

assert timed_priority(R3) [FD= R3System
}

Using a similar pattern to the previous processes, process R3 initially behaves nondeterministically. It can be interrupted by either VCModule_obstacle.in.Loc_left or VCModule_obstacle.in.Loc_right, where, as before, in indicates this is an input to the software, and Loc_left and Loc_right indicate that an obstacle is detected on either the left or right of the robot, specified using a data type in RoboChart. It can then behave as either ChangeDirectionOp, that models the call to the RoboChart operation ChangeDirection, or ReverseOp, that models the call to Reverse, followed by the recursion on R3.

Observe that ChangeDirection is a software operation, and as such, it interfaces with the platform by calling either TurnLeft or TurnCall, as specified in the CSP process ChangeDirectionOp. Here we simply record that either operation can be called nondeterministically, since R3 does not specify a particular direction.

Both calls to ChangeDirection and Reverse do not consume time, and thus are specified outside the timed section.

As before, the requirement is stated using a refinement check, but in this case the System process is composed in parallel with SKIP, synchronising on VCModule_cmd, indicating that no command can be issued, and VCModule_odometer is hidden.

R4: While no command is issued, if an obstacle is detected, an odometer should be read.

This requirement is encoded in CSP as follows.

Timed(OneStep) {
R4 = CHAOS(Events)
     [| {|VCModule_obstacle.in.Loc_left, VCModule_obstacle.in.Loc_right|} |>
     (Deadline(VCModule_odometer.in?x -> SKIP,0) ; R4)

R4System = (System [| {|VCModule_cmd|} |] SKIP)

assert timed_priority(R4) [FD= timed_priority(R4System)
}

Similar to the previous processes, R4 is specified using an interrupt on events VCModule_obstacle.in.Loc_left and VCModule_obstacle.in.Loc_right. Following such an event, the

RoboChart Model

The RoboChart model consists of a module named VCModule, connecting the events of platform VCRobot to controller named VCController. There are 5 input events: odometer of type natural that corresponds to an odometer reading; obstacle of type Loc, also defined in RoboChart, that identifies the location of an obstacle relative to the robot left, right or no obstacle; turn that is used by the platform to instruct the controller to turn; found to indicate whether the charging station has been found; cmd for the robot to be stopped. There is a single output event flash that is used for the controller to activate LEDs on the robot.

The robotic platform VCRobot uses the input and output events, defined in an interface Events, and provides two interfaces: OperationSig that contains operations implemented by the platform, and OperationDef containing a single operation ChangeDirection that is actually defined in RoboChart in terms of lower level operations in OperationSig. All operations in OperationSig are specified as terminating.

The controller VCController requires both interfaces OperationSig and OperationDef, and uses the interface Events. The input and output events are connected to a state machine Movement.

The structure of the controller and the robotic platform are the same throughout this document. In what follows we focus our attention on the definition of the first version of the state machine Movement.

Version 1 (download)

The state machine Movement also requires the interfaces OperationSig, OperationDef and uses the interface Events. In addition, it defines a number of constants: outPeriod, stuckDist, turningPeriod, batteryLife and forwardPeriod. It also defines 5 variables: angle, d0, d1, l and l_new. Finally, two clocks T1 and T2 are also defined. It consists of two states, Searching and Finish.

Analysis

To check that the refinements hold, the constants specified in RoboChart, as well as bounds for the data types need to be provided in order for model checking to be performed. Below we describe their values.

#### Parameters for model-checking. For analysis the process System is manually defined in the file ManualAssertions.csp as:

System = timed::VCModule(1)

it is defined as the automatically calculated timed semantics of RoboChart as timed::VCModule(1), where 1 is a natural that uniquely identifies the module. Observe that this is simply an artifact of the semantics of RoboChart that provides support for specifying collections.

The data types and functions are instantiated as in the file instantiations.csp. Natural and real are instantiated as the set {0..2} for verification. Of particular importance is the definition of the constants outPeriod, stuckDist, batteryLife, turningPeriod and forwardPeriod, in addition to the definition of the function Length, all reproduced below.

-- generate Movement_outPeriod not
Movement_outPeriod = 1

-- generate Movement_stuckDist not
Movement_stuckDist = 1

-- generate Movement_batteryLife not
Movement_batteryLife = 1

-- generate Length not
Length(i,j) = if i-j < 0 then Neg(i-j,real) else Minus(i,j,real)

-- generate Movement_turningPeriod not
Movement_turningPeriod = 1

-- generate Movement_forwardPeriod not
Movement_forwardPeriod = 1

The assertions file is called ManualAssertions.csp within the folder src-gen/timed/ of a project (ie. its zip file).

Results

Discussion

Requirements R1 and R2 are satisfied, while R3 and R4 are not.

R3

The counter-example for R3, shown below,

timed_priority(tock)(R3) [FD= R3System:
    Log:
        Result: Failed
        Visited States: 6
        Visited Transitions: 17
        Visited Plys: 3
        Estimated Total Storage: 134MB
        Counterexample (Divergence Counterexample)
            Specification Debug:
                Trace: <MoveForwardCall, MoveForwardRet,
                VCModule_obstacle.in.Loc_left>
            Implementation Debug:
                R3System (Repeat Behaviour):
                    Trace: <MoveForwardCall, MoveForwardRet,
                    VCModule_obstacle.in.Loc_left>
                    Repeats the trace: <τ>

indicates that following the trace <MoveForwardCall, MoveForwardRet, VCModule_obstacle.in.Loc_right> there is a divergence. This is because there is an unreasonable assumption that there can be an infinite number of odometer readings in a finite amount of time. Therefore, we propose a new version of R3System as R3System' where the number of odometer readings within a single time unit is bounded to at most 2.

Bounded(S,N) = BoundedIni(S,N,N)

BoundedIni(S,N,I) = if N == 0 then tock -> Bounded(S,I)
                              else tock -> BoundedIni(S,I,I)
                                   []
                                   ([] x:S @ x -> BoundedIni(S,N-1,I))
Timed(OneStep) {

R3System' = timed_priority(((System [| {|VCModule_cmd|} |] SKIP)
                           [| {|VCModule_odometer,tock|} |]
                           Bounded({|VCModule_odometer|},2)) \{|VCModule_odometer|})
}

This is achieved by composing in parallel with (System [| {|VCModule_cmd|} |] SKIP) a process Bounded({|VCModule_odometer|},2), synchronising on the channel set VCModule_odometer and the event tock, that only offers VCModule_odometer at most twice before time elapses.

The new assertion is then

assert timed_priority(R3) [FD= R3System'

and as required it passes.

So the revised table of results is presented below.

R4

The verification of requirement R4 fails, as detailed below.

timed_priority(tock)(R4) [FD= R4System:
    Log:
        Result: Failed
        Visited States: 6
        Visited Transitions: 15
        Visited Plys: 3
        Estimated Total Storage: 134MB
        Counterexample (Trace Counterexample)
            Specification Debug:
                Trace: <MoveForwardCall, MoveForwardRet,
                VCModule_obstacle.in.Loc_left>
                Available Events: {|VCModule_odometer.in|}
            Implementation Debug:
                R4System (Trace Behaviour):
                    Trace: <MoveForwardCall, MoveForwardRet,
                    VCModule_obstacle.in.Loc_left>
                    Error Event: ChangeDirectionCall

In this case we have that after calling MoveForward and noticing an obstacle the system can perform a call to ChangeDirection, whereas the requirement actually requires an odometer reading to take place before a call to either ChangeDirection or Reverse. In this case, and despite our earlier discussion earlier on the failure of R3, it is the model of state machine SMovement that is at fault. So we propose a new version in the following section.

Version 2 (download)

To ensure that an odometer reading follows an obstacle detection we change states Avoiding and AvoidingAgain as follows.

Analysis

As before, the parameters used in the instantiations.csp file are exactly the same.

Results

Discussion

Note that, because of the change in the model, whereby odometer readings are now performed only once in the entry action of states Avoiding and AvoidingAgain, requirement R3 is successfully met irrespective of the assumptions we considered for version 1 of the model. This is because there is no longer the possibility for the state machine to keep reading the odometer infinitely fast.

Similarly to the situation with version 1 of the model, all requirements pass, except for R4, as detailed below.

timed_priority(tock)(R4) [FD= R4System:
    Log:
        Result: Failed
        Visited States: 9
        Visited Transitions: 19
        Visited Plys: 4
        Estimated Total Storage: 0B
        Counterexample (Trace Counterexample)
            Specification Debug:
                Trace: <MoveForwardCall, MoveForwardRet,
                VCModule_obstacle.in.Loc_left>
                Available Events: {|VCModule_odometer.in|}
            Implementation Debug:
                R3Spec (Trace Behaviour):
                    Trace: <MoveForwardCall, MoveForwardRet,
                    VCModule_obstacle.in.Loc_left, τ>
                    Error Event: tock

FDR provides a counter-example whereby after calling the operation MoveForward and detecting an obstacle it is possible for time to pass, whereas the specification R4 required the odometer reading to be immediate. To rectify this problem, we impose a deadline of zero time on this reading on the entry action of states Avoiding and AvoidingAgain. Thus, we have a new version of the state machine SMovement, which we show in the following section.

Version 3 (download)

To accommodate the deadline of requirement R4, we update the entry actions of states Avoiding and AvoidingAgain to require the odometer reading to be completed immediately.

Analysis

Following the modifications in the third version, it is possible to check that all requirements are satisfied.

Results

The table of all results is shown below.

Simulation

The automatically generated code for simulation with ArGoS is available for download.