This report documents the RoboChart model of a robotic solar panel cleaner. It was developed as part of the final year project of Bianca Darolti at the Department of Computer Science at the University of York.
The model is available for download here. The report is available here.
assertion noFall : PathPlanningSM refines NoFall in the traces model with constants
cliff set to 1,
nozzle set to 1,
battery_low set to 0,
sleep_time set to 1,
acc_distance set to 1
csp NoFall csp-begin
Recurse(S,P) = [] ev : S @ ev -> P
NRecurse(S, P) = |~| ev : S @ ev -> P
Wait = Recurse({|PathPlanningSM_move_forward.out, PathPlanningSM_turn.out.Direction_left,
PathPlanningSM_turn.out.Direction_right, PathPlanningSM_clean.out.true, PathPlanningSM_clean.out.false,
PathPlanningSM_charging.in, PathPlanningSM_stop.out, PathPlanningSM_displacement.in,
PathPlanningSM_displacement.out, PathPlanningSM_battery_level.in|}, Wait)
[]
PathPlanningSM_ultrasonic.in?u -> CheckCliff(u)
CheckCliff(u) = let PathPlanningSM_cliff = 1 within
if u < PathPlanningSM_cliff then Wait
else
PathPlanningSM_turn.out!Direction_left -> TurnedLeft
[]
PathPlanningSM_turn.out!Direction_right -> TurnedRight
TurnedLeft = PathPlanningSM_move_forward.out -> Wait
[]
PathPlanningSM_turn.out.Direction_left -> TurnedBack
TurnedRight = PathPlanningSM_move_forward.out -> Wait
[]
PathPlanningSM_turn.out.Direction_right -> TurnedBack
TurnedBack = PathPlanningSM_move_forward.out -> Wait
[]
PathPlanningSM_turn.out.Direction_left -> Wait
NoFall = Wait ||| RUN({tock})
csp-end
assertion returnToCharge : PathPlanningSM refines ReturnToCharge in the traces model with constants
cliff set to 1,
nozzle set to 1,
battery_low set to 0,
sleep_time set to 1,
acc_distance set to 1
csp ReturnToCharge csp-begin
WaitBattery = Recurse({|PathPlanningSM_move_forward.out, PathPlanningSM_turn.out.Direction_left,
PathPlanningSM_turn.out.Direction_right, PathPlanningSM_clean.out.true,
PathPlanningSM_clean.out.false, PathPlanningSM_charging.in,
PathPlanningSM_stop.out, PathPlanningSM_displacement.out,
PathPlanningSM_displacement.in, PathPlanningSM_ultrasonic.in|},
WaitBattery)
[]
PathPlanningSM_battery_level.in?b -> CheckBattery(b)
CheckBattery(b) = let PathPlanningSM_battery_low = 0 within
PathPlanningSM_turn.out!Direction_left ->
if b > PathPlanningSM_battery_low then Wait
else Return
Return = PathPlanningSM_turn.out!Direction_left -> PathPlanningSM_move_forward.out ->
PathPlanningSM_clean.out!false -> Dock
Dock = PathPlanningSM_ultrasonic.in?u ->
if u < PathPlanningSM_cliff then Dock
else PathPlanningSM_turn.out!Direction_left -> PathPlanningSM_move_forward.out ->
PathPlanningSM_charging.in -> WaitBattery
ReturnToCharge = WaitBattery ||| RUN({tock})
csp-end
assertion returnAfterCharging : PathPlanningSM refines ReturnAfterCharging in the traces model with constants
cliff set to 1,
nozzle set to 1,
battery_low set to 0,
sleep_time set to 1,
acc_distance set to 1
csp ReturnAfterCharging csp-begin
CycleStart(n, MAX) = Recurse({|PathPlanningSM_move_forward.out, PathPlanningSM_turn.out.Direction_left,
PathPlanningSM_turn.out.Direction_right, PathPlanningSM_clean.out.true,
PathPlanningSM_clean.out.false, PathPlanningSM_battery_level.in|},
CycleStart(n, MAX))
[]
PathPlanningSM_ultrasonic.in?u -> CycleStart(n, MAX) [] CycleEnd(n, MAX)
[]
PathPlanningSM_displacement.out!0 -> CycleStart(n, MAX) [] CycleEnd(n, MAX)
[]
PathPlanningSM_displacement.in?d -> CycleStart(n, MAX)
CycleEnd(n, MAX) = Recurse({|PathPlanningSM_move_forward.out, PathPlanningSM_turn.out.Direction_left,
PathPlanningSM_turn.out.Direction_right, PathPlanningSM_clean.out.true,
PathPlanningSM_clean.out.false, PathPlanningSM_displacement.out|},
CycleEnd(n, MAX))
[]
PathPlanningSM_ultrasonic.in?u -> CycleEnd(n, MAX) [] ReturnToDock(0, MAX)
[]
PathPlanningSM_battery_level.in?b -> CycleEnd(n, MAX) [] ReturnToDock(n, MAX)
[]
PathPlanningSM_displacement.in?d -> CycleEnd(n, MAX) [] CheckEnd(n, MAX)
ReturnToDock(n, MAX) = Recurse({|PathPlanningSM_move_forward.out, PathPlanningSM_turn.out.Direction_left,
PathPlanningSM_turn.out.Direction_right, PathPlanningSM_clean.out.true,
PathPlanningSM_clean.out.false, PathPlanningSM_ultrasonic.in,
PathPlanningSM_battery_level.in, PathPlanningSM_displacement.in,
PathPlanningSM_displacement.out|},
ReturnToDock(n, MAX))
[]
PathPlanningSM_charging.in -> ExitDock(n, MAX)
CheckEnd(n, MAX) = if n < MAX then CycleStart(n+1, MAX) else ReturnToDock(0, MAX)
channel signal
channel cyclecount: int
ExitDock(n, MAX) = Recurse({|PathPlanningSM_stop.out, PathPlanningSM_turn.out|}, ExitDock(n, MAX))
[]
PathPlanningSM_move_forward.out -> Resume(n, MAX)
Resume(n, MAX) = PathPlanningSM_turn.out!Direction_right -> PathPlanningSM_move_forward.out ->
PathPlanningSM_displacement.out!0 -> cyclecount!n -> signal -> CycleStart(n, MAX)
WaitForCycles = PathPlanningSM_displacement.in?d -> WaitForCycles
[]
cyclecount?x -> Measure(x)
Measure(x) = PathPlanningSM_displacement.in?d ->
if d < x * PathPlanningSM_nozzle * 2 then Measure(x)
else signal -> WaitForCycles
ReturnAfterCharging = (Resume(0, 1) [|{|cyclecount, signal|}|] WaitForCycles)
\ {|cyclecount, signal|} ||| RUN({tock})
csp-end
assertion movementShape : PathPlanningSMMovements refines MovementShape in the traces model
csp PathPlanningSMMovements csp-begin
P_PathPlanningSM = let
PathPlanningSM_cliff = 1
PathPlanningSM_nozzle = 1
PathPlanningSM_battery_low = 0
PathPlanningSM_sleep_time = 1
PathPlanningSM_acc_distance = 1
within PathPlanningSM_O(0, PathPlanningSM_cliff, PathPlanningSM_nozzle,
PathPlanningSM_battery_low, PathPlanningSM_sleep_time,
PathPlanningSM_acc_distance)
PathPlanningSMMovements = P_PathPlanningSM \ {|PathPlanningSM_displacement.in, PathPlanningSM_displacement.out,
PathPlanningSM_ultrasonic.in, PathPlanningSM_battery_level.in,
PathPlanningSM_clean.out, PathPlanningSM_charging.in|}
csp-end
csp MovementShape csp-begin
ResumeCycling = PathPlanningSM_turn.out!Direction_right -> PathPlanningSM_move_forward.out -> Cycle
Cycle = PathPlanningSM_turn.out!Direction_left -> PathPlanningSM_move_forward.out ->
PathPlanningSM_turn.out!Direction_right -> PathPlanningSM_move_forward.out ->
Continue
Continue = PathPlanningSM_turn.out!Direction_right -> PathPlanningSM_move_forward.out ->
PathPlanningSM_turn.out!Direction_left -> PathPlanningSM_move_forward.out ->
(Cycle [] GoBack)
GoBack = PathPlanningSM_turn.out!Direction_left -> PathPlanningSM_turn.out!Direction_left ->
PathPlanningSM_move_forward.out -> PathPlanningSM_turn.out!Direction_left ->
PathPlanningSM_move_forward.out -> PathPlanningSM_stop.out ->
PathPlanningSM_turn.out!Direction_left -> PathPlanningSM_turn.out!Direction_left ->
PathPlanningSM_move_forward.out -> ResumeCycling
MovementShape = ResumeCycling ||| RUN({tock})
csp-end
assertion reachEnd : PathPlanningSMEndState refines ReachEnd in the failures model
csp PathPlanningSMEndState csp-begin
PathPlanningSMEndState = let
PathPlanningSM_cliff = 1
PathPlanningSM_nozzle = 1
PathPlanningSM_battery_low = 0
PathPlanningSM_sleep_time = 1
PathPlanningSM_acc_distance = 1
within
PathPlanningSM_VS_O(0, PathPlanningSM_cliff,
PathPlanningSM_nozzle, PathPlanningSM_battery_low,
PathPlanningSM_sleep_time, PathPlanningSM_acc_distance)
|\ {|PathPlanningSM_enteredV."PathPlanningSM_Go_right_again",
PathPlanningSM_enteredV."PathPlanningSM_Return",
PathPlanningSM_ultrasonic.in|}
csp-end
csp ReachEnd csp-begin
WaitGoRightAgain = PathPlanningSM_ultrasonic.in$u -> WaitGoRightAgain
|~|
PathPlanningSM_enteredV."PathPlanningSM_Go_right_again" -> CheckPanelEdge
|~|
PathPlanningSM_enteredV."PathPlanningSM_Return" -> WaitGoRightAgain
CheckPanelEdge = PathPlanningSM_ultrasonic.in$u ->
if u < PathPlanningSM_cliff then WaitGoRightAgain
else PathPlanningSM_enteredV."PathPlanningSM_Return" -> WaitGoRightAgain
ReachEnd = WaitGoRightAgain
csp-end
assertion cleanAllPanels : PathPlanningSM refines CleanAllPanels in the failures model
csp CleanAllPanels csp-begin
FacingUp = NRecurse({|PathPlanningSM_stop.out, PathPlanningSM_move_forward.out,
PathPlanningSM_ultrasonic.in, PathPlanningSM_displacement.in,
PathPlanningSM_displacement.out, PathPlanningSM_battery_level.in,
PathPlanningSM_charging.in, PathPlanningSM_clean.out|},
FacingUp)
|~|
PathPlanningSM_turn.out.Direction_left -> FacingLeft
|~|
PathPlanningSM_turn.out.Direction_right -> FacingRight
FacingLeft = NRecurse({|PathPlanningSM_stop.out, PathPlanningSM_move_forward.out,
PathPlanningSM_ultrasonic.in, PathPlanningSM_displacement.in,
PathPlanningSM_displacement.out, PathPlanningSM_battery_level.in,
PathPlanningSM_charging.in, PathPlanningSM_clean.out|},
FacingLeft)
|~|
PathPlanningSM_turn.out.Direction_left -> FacingDown
|~|
PathPlanningSM_turn.out.Direction_right -> FacingUp
FacingDown = NRecurse({|PathPlanningSM_stop.out, PathPlanningSM_move_forward.out,
PathPlanningSM_ultrasonic.in, PathPlanningSM_displacement.in,
PathPlanningSM_displacement.out, PathPlanningSM_battery_level.in,
PathPlanningSM_charging.in, PathPlanningSM_clean.out|},
FacingDown)
|~|
PathPlanningSM_turn.out.Direction_left -> FacingRight
|~|
PathPlanningSM_turn.out.Direction_right -> FacingLeft
FacingRight = NRecurse({|PathPlanningSM_stop.out, PathPlanningSM_move_forward.out,
PathPlanningSM_displacement.in, PathPlanningSM_displacement.out,
PathPlanningSM_battery_level.in, PathPlanningSM_charging.in,
PathPlanningSM_clean.out|},
FacingRight)
|~|
PathPlanningSM_turn.out.Direction_left -> FacingUp
|~|
PathPlanningSM_turn.out.Direction_right -> FacingDown
|~|
PathPlanningSM_ultrasonic.in?u -> CheckUltrasonic(u)
CheckUltrasonic(u) = if u < PathPlanningSM_cliff then FacingRight
else (
PathPlanningSM_turn.out.Direction_left -> FacingUp
|~|
PathPlanningSM_turn.out.Direction_right -> FacingDown
)
CleanAllPanels = FacingUp ||| CHAOS({tock})
csp-end
Requirement | Result (untimed) | Result (timed) |
---|---|---|
R1 | pass | pass |
R2 | pass | pass |
R3 | pass | pass |
R4 | pass | pass |
R5 | fail | fail |
R6 | pass | pass |
The model is available for download here.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500
University of York legal statements