Autonomous Chemical Detector

1. Introduction
2. Version 1.0
3. Version 2.0
4. Version 3.0
5. Version 4.0

Introduction

This report documents the development of the autonomous version of the chemical detector. Chapter 1 presents the initial model of the autonomous chemical detector, and identifies issues that hinder the verification of properties. Chapter 2 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. Chapter 3 further changes the model to establish the requirements below. Chapter 4 discusses a optimisation of the model based on removing local variables.

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

Requirement	Result
A.1 GasAnalysis deterministic	true
A.2 GasAnalysis divergence free	true
A.3 GasAnalysis deadlocks only after stop	true
A.4 Movement divergence free	true
A.5 Movement deadlocks only after flag	false
A.6 ChemicalDeterctor deadlocks only after termination	false
B.1 Every gas reading leads to a command	true
B.2 Every commands causes a reaction	false, resume can happen without a reaction
B.3 No gas, no termination	true

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

Requirement	Result
A.1 GasAnalysis deterministic	true
A.2 GasAnalysis divergence free	true
A.3 GasAnalysis deadlocks only after stop	true
A.4 Movement divergence free	true
A.5 Movement deadlocks only after flag	true
A.6 ChemicalDeterctor deadlocks only after termination	true
B.1 Every gas reading leads to a command	true
B.2 Every commands causes a reaction	false, resume can happen without a reaction
B.3 No gas, no termination	true

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.