Autonomous Chemical Detector

1. Introduction
2. Autonomous Chemical Detector 1
3. Autonomous Chemical Detector 2
4. Autonomous Chemical Detector 3
5. Autonomous Chemical Detector: state variable removal
6. Autonomous Chemical Detector: assertion language

Introduction

This page documents the development of the autonomous version of the chemical detector. Section 2 presents the initial model of the autonomous chemical detector, and identifies issues that hinder the verification of properties. Section 3 presents an updated version of the model that abstracts away some of the data types to allow the model checking of basic properties and identify some mistakes. Section 4 further changes the model to establish the requirements below. Section 5 discusses a optimisation of the model based on removing local variables. Section 6 then shows how the requirements stated below can be expressed in our assertions language so they can be automatically checked.

As a basis for verification, we define a few requirements for the autonomous chemical detector and encode them as CSP processes:

A) Basic Requirements

1) GasAnalysis is deterministic.

2) GasAnalysis is divergence free.

3) GasAnalysis should deadlock only on arrival of a stop event.

4) Movement is divergence free.

5) Movement should deadlock only on arrival of a flag event.

6) ChemicalDetector should deadlock only on termination of individual controllers.

To check that deadlock occurs only in special circumstances as in requirements 3, 6, and 7, we consider a parallelism. For instance, we analyse ChemicalDetector in parallel with a special process flag -> DONE, where DONE = done -> DONE, is deadlock free.

channel done

DONE = done -> DONE

assert ChemicalDetector_O [| {|flag|} |] flag -> DONE :[deadlock free]

B) Model Requirements

1) Every gas reading should lead to a command resume, stop or turn.

The machine can terminate instead of receiving a gas reading.

Spec1 =
GasAnalysis_gas?x -> (
|~|e:{|GasAnalysis_resume, GasAnalysis_stop, GasAnalysis_turn|} @ e->Spec1
)
|~|
SKIP

assert Spec1 [FD= GasAnalysis

2) Every command to move the robot (resume, stop, turn) leads to a reaction by the robot, before another command is issued.

Spec2 = let
Init = randomWalkCall -> randomWalkRet -> SKIP |~| randomWalkCall -> SKIP |~| SKIP
Reaction = |~|e:{|moveCall, moveRet, randomWalkCall, randomWalkRet, flag, obstacle, odometer|} @ e->(Reaction|~|SKIP)
T = (SKIP |~| (|~|e:{|Movement_resume, Movement_turn,Movement_stop|} @ e->SKIP); Reaction; T)
within
Init ||| T

assert Spec2 [FD= Movement_O

3) If there is no gas, the chemical detector does not terminate.

NoGas = gas.<(0,0)> -> NoGas

assert ChemicalDetector_O [| {|gas|} |] NoGas :[deadlock free]

Autonomous Chemical Detector 1 (download)

In order to support model checking, RoboTool instantiates core types such as nat as {0,1} and real as {-1,0,1}, but the model uses values such as -90, 90 and 180 in channels of type real, which leads to errors in the generated model.

It is possible to edit the generated code to instantiate the types with a larger range of values that avoids this error. For example, real can be defined as {-90..180}. This change, however, leads to a state explosion, and, in order to avoid this problem, we define an abstract type using enumerations in the next chapter.

Model

For this example, the module ChemicalDetector is shown below, where we have a robotic platform Vehicle and controllers MainController and MicroController.

-- generate intensity not
intensity(<>) = 0
intensity(<(c,i)>^xs) = let
n = intensity(xs)
within if (n > i) then n else i

-- generate location not
--location :: (<Chem.Intensity>) -> real
location(gs) = let
find(<>,_) = 0
find(<(c,i)>^xs,n) = if (i == intensity(gs)) then n else find(xs,n+1)
within
if (length(gs) > 0) then (360/length(gs))*find(gs,0) else 0

-- generate analysis not
analysis(gs) = if (intensity(gs) > 0) then gasD else noGas

-- generate greater not
greater(i1,i2) = i1 > i2

-- generate Angle not
nametype Angle = {0,180}

Autonomous Chemical Detector 2 (download)

To avoid the problem found in the previous chapter, we abstracted the type of the values associated with turning the robot to an enumeration Angle containing four values. In this case, it is possible to check the requirements identified in the introduction.

Tthree requirements fail: A.5, A.6 and B.2, as shown in the table below. We address the first two problems in the next version of the model that we present in the next chapter. The third is a timing issue, and we do not cover here.

The failure of requirement A.5 gives a counterexample that shows that the machine Movement is not prepared to treat commands resume, turn and stop in certain states. For example, while in the state Avoiding, the only acceptable command is turn, but turn is only produced by GasAnalysis if some gas is detected, but not above a threshold. If no gas is detected, or if the intensity is above the threshold, gas analysis would send a resume command or a stop command, neither of which Avoiding is prepared to treat. Furthermore, these events will not be treatable until a turn happens, which might not be possible. This can be solved by adding transitions to most states to allow the treatment of events stop and resume. The failure of requirement A.6 is a consequence of the failure of requirement A.5.

In the next chapter, we add the missing transitions and re-analyse the model. Alternatively, it may be possible to prove that, given appropriate implementations of the functions analysis, location and angle, only the correct order of commands is produced. We have not pursued this option here, though.

While A.5 is not a trivial problem to debug, the cause of B.2 is clearer. The reason two resume events can happen in sequence is because the operation randomWalk is called in the during action, which means the potential reaction to resume can immediately be interrupted by another resume event. This violation is due to missing timing information regarding the occurrences and processing of gas readings.

Model

Analysis

Autonomous Chemical Detector 3 (download)

In this model, we add a number of extra transitions to the Movement state machine to avoid the deadlock scenarios identified in the previous chapter. In particular, states with a single transitions guarded by turn need these extra transitions. These changes are not sufficient to guarantee termination, additionally the operation move needs to be further specified to indicate it terminates. After this change, the model satisfies all the requirements, except B.2, which is caused by missing timing information in the model, but is beyond the scope of this report and is left as future work.

Further analysis uncover another problem in the model. While all states of the state machines are reachable when the state machines are analysed in isolation, the same is not true for their composition in the module ChemicalDetector. In particular, the state GettingOut is no longer reachable for the module. This error traces to the default value assigned to the unspecified constant thr of the state machine GasAnalysis. Our generator assigns 0 as a default value for numerical constants, and this value causes one of the transitions of GasAnalysis to be always true (and the other always false) leading to terination as soon as possible, which causes the Movement state machine to also terminate as soon as possible, thus bypassing the state GettingOut. Changing the value of thr to 1 is enough to make all state reachable, but reveals a further issue with termination of ChemicalDetector. This is caused by the use of the potentiall non-terminating operation randomWalk in the entry action of the state GettingOut. We replace the call to randomWalk by a call to shortRandomWalk that is guaranteed to terminate, and the ChemicalDetector can be shown to terminate.

Model

Analysis

Autonomous Chemical Detector: state variable removal (download)

In this chapter, we describe a simple strategy to remove state variables under certain conditions. To illustrate this, we show the gas analysis state machine, in which the state machine variables a, i and st are used locally to improve readability of the model. These variables can be removed to reduce the size of the state space generated by the model, which, depending on the types associated with these variables, can lead to significant improvement in compilation and analysis times in FDR.

We have verified that the state machine GasAnalysis of this Chapter and the one in Chapter 2 are equivalent. Furthermore, while the property check times¹ for the two versions of the state machines are similar (0.03s for Chapter 2 and 0.05s for Chapter 4), the compilation times are radically different. The state machine in Chapter 2 takes 12.55s to compile (before the check can be performed), while the state machine in Chapter 4 (without the redundant state variables) takes 0.54s to compile. This analysis was performed by instantiating primitive sets to contain only 3 values, and limiting the size of sequences to at most 2.

If we increase the maximum size of sequences to 3, the state machine in Chapter 2 no longer compiles as the machine runs out of memory². The machine in Chapter 4, on the other hand, manages to compile in 84.33s and perform the property check in 0.03s.

This suggests that eliminating redundant state variables is an effective strategy, even when none of the eliminated variables individually cause state explosion. In our example, the main cause for long compilation times is the variable gs (and events communicating sequences) as indicated by the difference in compilation times by the increase in the maximum size of sequences. Nevertheless, the elimination of variables that only communicate values drawn from small sets (size 3) has a significant impact on the compilation phase.

Autonomous Chemical Detector: assertion language (download)

Requirements

This model was created and analysed using the following version of the RoboTool plugins:

In this section, we present an updated version of the Autonomous Chemical Detector model that works with the latest version of the RoboChart editors and CSP generator. This model uses the RoboChart assertion langauge to specify some of the properties in a more user friendly way. Below, we show all of the diagrams including some updates and discuss the assertions.

Diagrams

The functions pre and post conditions have been updated to use the appropriate sequence limits, which starts at 1 (instead of 0).

Previous versions of this model had two transitions out of Avoiding triggered by the resume event. This has been fixed in this model with the transition moved from Avoiding to Going and targeting Waiting.

Assertions

The assertions discusses in the introduction have been specified in the assertion language provided by RoboTool (file properties.assertions). Some of these assertions can be modelled directly in the assertion langauge, while others have to be specified partially in CSP within a special CSP block.

A) Basic Requirements

1) GasAnalysis is deterministic.

assertion A1: GasAnalysis is deterministic.

2) GasAnalysis is divergence free.

assertion A2: GasAnalysis is divergence-free.

3) GasAnalysis should deadlock only on arrival of a stop event.

csp SpecA3 associated to GasAnalysis csp-begin
    channel done3
    DONE3 = done3 -> DONE3
    SpecA3 = GasAnalysis::O__(0,const_GasAnalysis_thr) [| {|GasAnalysis::stop|} |] GasAnalysis::stop.out -> DONE3
csp-end

assertion A3: SpecA3 is deadlock-free.

4) Movement is divergence free.

assertion A4: Movement is divergence-free.

5) Movement should deadlock only on arrival of a flag event.

csp SpecA5 associated to Movement csp-begin
    channel done5
    DONE5 = done5 -> DONE5
    SpecA5 = Movement::O__(0, const_Movement_lv, const_Movement_evadeTime, const_Movement_stuckPeriod, const_Movement_stuckDist, const_Movement_outPeriod) [| {|Movement::flag|} |] Movement::flag.out -> DONE5
csp-end

assertion A5: SpecA5 is deadlock-free.

6) ChemicalDetector should deadlock only on termination of individual controllers.

untimed assertion A6: ChemicalDetector terminates.

B) Model Requirements

1) Every gas reading should lead to a command resume, stop or turn.

The machine can terminate instead of receiving a gas reading.

csp SpecB1 associated to GasAnalysis csp-begin
    SpecB1 = GasAnalysis::gas?x -> (
	    |~|e:{|GasAnalysis::resume, GasAnalysis::stop, GasAnalysis::turn|} @ e->SpecB1
    )
    |~|
    STOP
    |~|
    GasAnalysis::terminate -> SKIP
csp-end

untimed assertion B1: GasAnalysis refines SpecB1

2) Every command to move the robot (resume, stop, turn) leads to a reaction by the robot, before another command is issued.

This specification has been modified to allow resume to happen without a reaction; this exception had been identified in a previous version of the model.

csp SpecB2 associated to Movement csp-begin
    SpecB2 = let
    	Init = SKIP |~| Movement::randomWalkCall -> SKIP
    	Reaction = |~|e:{|Movement::moveCall, Movement::randomWalkCall, Movement::flag|} @ e->(Reaction|~|SKIP)
	    T = (SKIP |~| (|~|e:{|Movement::turn,Movement::stop, Movement::resume|} @ e->SKIP); Reaction; T)
	    Chaos = STOP |~| (|~| e: {|Movement::obstacle, Movement::odometer, Movement::changeDirectionCall, Movement::shortRandomWalkCall, Movement::resume|} @ e -> Chaos) |~| Movement::terminate -> SKIP
    within
    	(Init ||| T ||| Chaos)
csp-end

untimed assertion B2: Movement refines SpecB2

3) If there is no gas, the chemical detector does not terminate.

csp SpecB3 associated to ChemicalDetector csp-begin
	NoGas = ChemicalDetector::gas.in.<(0,0)> -> NoGas
	SpecB3 = ChemicalDetector::O__(
				0,
				const_MicroController_stm_ref0_lv,
				const_MicroController_stm_ref0_evadeTime,
				const_MicroController_stm_ref0_stuckPeriod,
				const_MicroController_stm_ref0_stuckDist,
				const_MicroController_stm_ref0_outPeriod,
				const_MainController_stm_ref0_thr,
				const_Location_changeDirection_lv
	) [| {|ChemicalDetector::gas|} |] NoGas
csp-end

assertion B3: SpecB3 is deadlock-free.

Analysis

The results below have been automatically checked using FDR and summarised in the tables below by RoboTool.

Results of untimed analysis of assertions in properties.assertions using FDR

Results of timed analysis of assertions in properties.assertions using FDR

Footnotes