Department of Computer Science

Solar Panel Vacuum Cleaner

Introduction

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.

Requirements

R1

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

R2

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

R3

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

R4

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

R5

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

R6

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

RoboChart Model

Analysis

Results

Requirement Result (untimed) Result (timed)
R1 pass pass
R2 pass pass
R3 pass pass
R4 pass pass
R5 fail fail
R6 pass pass

Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500