Environmental Sensing

This report documents the development of an environmental sensing robot. The following sections presents the RoboChart model, whose RoboTool project is available for download, the basic requirements, and the the verification results.

RoboChart Model (download)

Basic Requirements

The basic requirements presented in this section are encoded using the assertion facilities of RoboTool in a file test.assertion.

EnvironmentalSensing is deadlock-free

This is specified as assertion EnvironmentalSensing is deadlock-free (r1).

EnvironmentalSensing terminates

This is specified as assertion EnvironmentalSensing terminates (r2).

Commands received by the MicroController always lead to reactions by the robot, before another command can be accepted

csp Spec2 csp-begin
	include "../defs/Chemical_defs.csp"
Spec2 = let
	Init = moveForwardCall -> moveForwardRet -> SKIP |~| moveForwardCall -> SKIP |~| SKIP
	Reaction = |~|e:{|moveForwardCall, moveForwardRet, moveTowardsCall, moveTowardsRet, Movement_flag, Movement_obstacle, Movement_odometer|} @ e->(Reaction|~|SKIP)
	T = (Reaction |~| SKIP |~| (|~|e:{|Movement_resume, Movement_turn,Movement_stop|} @ e->SKIP); Reaction; T)
	Clock = (tock -> SKIP |~| SKIP); Clock
within
	Init ||| T ||| Clock
csp-end

The analysis of this requirement is specified by the following assertion:

assertion Movement refines Spec2 (r3)

Analysis

Since our example uses various timed constructs, our initial verification is performed in the timed model using FDR and tock-CSP. This is necessary because the untimed semantics of timed constructs introduces nondeterministic choices and deadlocks to model all possible behaviours that the timed semantics can express more precisely.

In our initial analysis, we are interested in two properties: deadlock freedom and termination. Verification using FDR shows that our example is not deadlock free, but terminates successfully. These two properties associated with the fact that FDR inteprets termination as deadlock, and our special encoding of the termination check, show that our model does not deadlock due to concurrency problems, but only in the event of termination of both controllers.