This page documents the RobChart and RoboSim Software and Physical Models of the SRanger example. It is a robot that moves in a straight line and then turns when it finds an obstacle. The RoboTool project is available for download here and includes the RoboChart and RoboSim models (software and physical models). The RoboWorld document is found here.

The tock-CSP semantics of the RoboChart model, as automatically calculated by RoboTool,
is found in the SRanger.zip archive in `csp-gen/timed/defs/SimFW.csp`

. A simplified version of that semantics, proved to be equivalent, is
typed in `RC_simplified.assertions`

. An excerpt
is reproduced below, where the main process is `Spec`

.

```
MinusNoNeg(e1,e2,T) = if e1-e2 > 0 then Minus(e1,e2,T) else 0
timed csp Spec csp-begin
Timed(OneStep) {
-- Simplified RoboChart semantics, written within a timed-section
-- Main process with maximal progress.
Spec = timed_priority(Initial)
Initial = EntryMoving;
Obs;
EntryTurning;
-- In the RoboChart model #MBC is reset after obstacle, so we need to subtract 2 units
-- from that, given that EntryTurning consumes, at least, 2 time units.
WAIT(MinusNoNeg(Div(const_SimFW_SMovement_PI,const_SimFW_SMovement_av,core_nat),2,core_nat));
Initial
EntryMoving = StartBy(SimFW::CMovement::moveCall.const_SimFW_SMovement_lv.0 -> WAIT(1),0)
Obs = SimFW::CMovement::obstacle.in -> SKIP
EntryTurning = StartBy(SimFW::CMovement::stopCall -> WAIT(1) ;
StartBy(SimFW::CMovement::moveCall.0.const_SimFW_SMovement_av -> WAIT(1),
0),
0)
-- For verification using tick-tock need to provide alphabet of Spec process,
-- which in this case is exactly the same as that of the built-in calculated
-- by RoboTool
Spec__sem__events = SimFW::CMovement::sem__events
}
csp-end
timed assertion A0 : SimFW::CMovement equals Spec
timed assertion A1 : SimFW::CMovement equals Spec in the tick-tock model
```

For verification with FDR, the file `csp-gen/timed/RC_simplified_assertions.csp`

should be loaded. It contains CSPM automatically generated by RoboTool from `RC_simplified.assertions`

.

A probabilistic junction is added to the RoboChart model above to allow for randomly choose to turn left or right when an obstacle is detected.

The probabilistic model can be found in the archive SRanger-probability.zip. The properties checked (considering `PI=3`

, `av=2`

, and `lv=1`

) are listed below and can be found in `prob_properties/prob.assertions`

in the archive. The verification report can be found in `prism-gen/20221104135200/prob_assertions.html`

in the archive.

`P_deadlock_free`

: deadlock freedom`P_reachable_TurningLeft`

: whether state`TurningLeft`

is reachable`P_reachable_TurningRight`

: whether state`TurningRight`

is reachable`P_prob_TurningRight`

: the probability that the state`TurningRight`

is eventually reached`P_always_TurningRight`

: whether state`TurningRight`

is always reachable`P_nr_obstacle`

: on average, how many`obstacle`

s before the state`TurningRight`

is eventually reached

Verification results:

** Please note that current analysis of probabilistic behaviour of this model using PRISM cannot deal with time semantics, and so this analysis ignores those time constructs. **

The model include a p-model, a d-model and the platform mapping that connects them. The used elements of the RoboSim library are also shown.

The tock-CSP semantics of the RoboSim software model, as automatically calculated by RoboTool,
is found in the SRanger.zip archive in `csp-gen/sim/defs/SimSMovement.csp`

. A simplified version of that semantics, proved to be equivalent, is
typed in `RS_simplified.rsa`

with
an excerpt reproduced below:

```
timed csp Spec csp-begin
Timed(OneStep) {
-- Simplified RoboSim semantics, written within a timed-section
-- Main process with maximal progress.
Spec = timed_priority(StartBy(SimCMovement::registerRead.SimCMovement::i_obstacle?x__ -> Initial,0))
Initial = SMoving;
DMoving;
Waiting;
STurning;
DTurning(1);
Initial
SMoving = StartBy(SimCMovement::registerWrite.SimCMovement::o_move.const_SimSMovement_lv.0 -> SKIP,0)
DMoving = WAIT(cycle_SimCMovement_SimCMovement);
StartBy(SimCMovement::registerRead.SimCMovement::i_obstacle?obstacle ->
if obstacle then
StartBy(SimCMovement::registerWrite.SimCMovement::o_stop -> SKIP,0)
else
DMoving,
0)
Waiting = WAIT(cycle_SimCMovement_SimCMovement)
STurning = StartBy(SimCMovement::registerRead.SimCMovement::i_obstacle?x__ ->
StartBy(SimCMovement::registerWrite.SimCMovement::o_move.0.const_SimSMovement_av -> SKIP,0)
,0)
-- Note the use of a parameter MBC to replicate the current value of the clock MBC
DTurning(MBC) = WAIT(cycle_SimCMovement_SimCMovement);
StartBy(SimCMovement::registerRead.SimCMovement::i_obstacle?x__ ->
if (MBC >= Div(const_SimSMovement_PI,const_SimSMovement_av,core_real)) then
SKIP
else
DTurning(MBC+1)
,0)
-- For verification using tick-tock need to provide alphabet of Spec process,
-- which in this case is exactly the same as that of the built-in calculated
-- by RoboTool
Spec__sem__events = SimCMovement::sem__events
}
csp-end
timed assertion A0 : SimCMovement equals Spec
timed assertion A1 : SimCMovement equals Spec in the tick-tock model
```

For verification with FDR, the file `csp-gen/sim/file_RS_simplified_assertions.csp`

should be loaded. It contains CSPM automatically generated by RoboTool from `RS_simplified.rsa`

.

The verification that the simulation is a correct implementation of the RoboChart
software model is specified within the file `checks.rsa`

containing the following:

```
simulation Sim of SimFW::CMovement {
cycleDef { cycle == 1 }
}
assertion A0 : SimCMovement refines Sim
assertion A1 : SimCMovement refines Sim in the tick-tock model
```

For verification with the FDR the corresponding CSPM file is `csp-gen/sim/file_checks_assertions.csp`

.

The hybrid semantics of the RoboSim p-model, partially calculated by RoboTool, is found here. The semantics is shown below:

```
// GLOBAL VARIABLES
// SRanger_Base_LHinge_F: vector(real,6)
// ...
const TimeScale: real, // This is the correspondence of a discrete time unit and the continous time (e.g., TimeScale = 5ms indicates that a tock in the d-model takes 5ms)
cycle: real | cycle == 1, // This comes from the definition of cycle
SRanger_Base_LHinge_AXIS: vector(real,3) = (|0,1,0|),
SRanger_Base_LHinge_S: vector(real,6) = ScrewAxis(SRanger_Base_LHinge_AXIS, Pitch::Finite(0)),
...
SRanger = var timer: real,
SRanger_Base_LHinge_pV: vector(real,6),
...
@ let
Init = SKIP
ResetTimer = timer := 0
SendToSoftware = (
(
if (SRanger_Base_IR_voltage>=3.0)
then registerRead.obstacle.true -> SKIP
else registerRead.obstacle.false -> SKIP
)
)
ReceiveFromSoftware = (
registerWrite.moveCall?lv?av -> (
{SRanger_Base_LHinge_LMotor_das, SRanger_Base_RHinge_RMotor_das}:[
(SRanger_Base_LHinge_LMotor_das==dsl)
and
(SRanger_Base_RHinge_RMotor_das==dsr)
and
(lv==RADIUS * (dsl + dsr) / 2)
and
(av==RADIUS * (dsl - dsr) / axisLength)
]
)
|||
registerWrite.stopCall -> (
{SRanger_Base_LHinge_LMotor_das, SRanger_Base_RHinge_RMotor_das}:[
(SRanger_Base_LHinge_LMotor_das==0)
and
(SRanger_Base_RHinge_RMotor_das==0)
]
)
)
Cycle = SendToSoftware; ReceiveFromSoftware /\ wait(cycle); ResetTimer;
var SRanger_Base_LHinge_theta: real,
SRanger_Base_LHinge_v: real,
...
@ (
// equations
SRanger_Base_IR_voltage == 4*exp(-0.028784*SRanger_Base_IR_distance)
and
SRanger_Base_LHinge_fV == AdT(SRanger_Base_LHinge_theta)*SRanger_Base_LHinge_pV
+
SRanger_Base_LHinge_A*SRanger_Base_LHinge_v
...
// the timer variable controls the execution of the cycle; it is reset at every cycle
timer' = 1
) /\ (
// domain condition
timer > TimeScale*cycle
); Cycle
within Init; Cycle
Simulation = (SRanger [|{|tock,registerRead,registerWrite|}|] SimCMovement)\{|tock,registerRead,registerWrite|}
```

A description of the RoboWorld model is available and a zip file with RoboWorld document for the ranger and lexicon files for the RoboWorld plugin is provided.

```
## ARENA ASSUMPTIONS ##
The arena is two-dimensional.
The arena has a floor.
The gradient of the ground is 0.0.
The arena has obstacles.
## ROBOT ASSUMPTIONS ##
The robot is a point mass.
## ELEMENT ASSUMPTIONS ##
The obstacles are circles.
The arena has at least 2 obstacles.
## MAPPING OF INPUT EVENTS ##
When the distance from the robot to an obstacle is less than 0.5 m, the event obstacle occurs.
## MAPPING OF OUTPUT EVENTS ##
## MAPPING OF OPERATIONS ##
When the operation move(lv,av) is called, the velocity of the robot is set to lv m/s in the direction of the orientation of the robot, and the angular velocity of the robot is set to av rad/s.
## MAPPING OF VARIABLES ##
```

A RoboCert script is available that encodes the sequence diagram below:

The script also carries an equivalent, but simplified, hand-written tock-CSP encoding of the property, and assertions to check its equivalence against that generated by RoboTool.

We also make the
RoboTool-generated translation to tock-CSP available
for reference (as this file depends on various other files generated and
copied by RoboTool, people wishing to verify the property should copy
the `.rcert`

file into the SRanger case study and use RoboTool to generate the
CSP afresh).

This model was created using the RoboSim Physical Modelling Graphical Editor version 3.0.0.

The CyPhyCircus model our RoboSim Physical models can be generated using a combination of the CyPhyCircus Generator, which produces the process algebraic component of the model and the robosim-solver, which calculates the continuous component. Currently, these need to be integrated by hand, but the CyPhyCircus generator is being extended to execute the robosim-solver internally and to incorporate its results into the complete hybrid model. The document robosim-solver-manual gives a brief overview of the tool and step by step instructions of how to use it.

The RoboCert development targets the RoboCert Textual Editor and Metamodel
version 0.1.0. Note that, when generating CSP from `properties.rcert`

, the
CSP will appear at `csp-gen/timed/robocert/pkg/properties.csp`

and can be
checked using FDR4. You may need to remove some definitions from
`csp-gen/timed/instantiations.csp`

for a successful compilation.

The probabilistic model could only be analysed using the RoboChart PRISM Generator and RoboChart Assertions plugins released after November 04, 2022.

Deramore Lane, University of York, Heslington, York, YO10 5GH, UK

Tel: 01904 325500

University of York legal statements