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:
GasAnalysis
is deterministic.GasAnalysis
is divergence free.GasAnalysis
should deadlock only on arrival of a stop event.Movement
is divergence free.Movement
should deadlock only on arrival of a flag event.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]
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
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
NoGas = gas.<(0,0)> -> NoGas
assert ChemicalDetector_O [| {|gas|} |] NoGas :[deadlock free]
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.
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}
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.
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 |
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.
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 |
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 times1 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 memory2. 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.
This model was created and analysed using the following version of the RoboTool plugins:
Plugin | Version |
---|---|
RoboChart Metamodel | 2.0.0.202105071032 |
RoboChart Textual Editor | 3.0.0.202107301304 |
RoboChart Graphical Editor | 2.0.0.202107272159 |
RoboChart Assertions | 2.0.0.202107301309 |
RoboChart CSP Generator | 3.0.0.202108031246 |
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.
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
.
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.
GasAnalysis
is deterministic.assertion A1: GasAnalysis is deterministic.
GasAnalysis
is divergence free.assertion A2: GasAnalysis is divergence-free.
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.
Movement
is divergence free.assertion A4: Movement is divergence-free.
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.
ChemicalDetector
should deadlock only on termination of individual controllers.untimed assertion A6: ChemicalDetector terminates.
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
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
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.
The results below have been automatically checked using FDR and summarised in the tables below by RoboTool.
Assertion | States | Transitions | Result |
---|---|---|---|
GasAnalysis is deterministic (A1) [failures divergences model] | 6 | 26 | true |
GasAnalysis is divergence free (A2) [failures divergences model] | 6 | 26 | true |
SpecA3 is deadlock free (A3) [failures divergences model] | 5 | 27 | true |
Movement is divergence free (A4) [failures divergences model] | 30 | 107 | true |
SpecA5 is deadlock free (A5) [failures divergences model] | 29 | 108 | true |
untimed ChemicalDetector terminates (A6) | 8 | 72 | true |
untimed GasAnalysis refines SpecB1 (B1) [failures divergences model] | 6 | 26 | true |
untimed Movement refines SpecB2 (B2) [failures divergences model] | 32 | 120 | true |
SpecB3 is deadlock free (B3) [failures divergences model] | 3 | 7 | true |
Assertion | States | Transitions | Result |
---|---|---|---|
GasAnalysis is deterministic (A1) [failures divergences model] | 548 | 1011 | true |
GasAnalysis is divergence free (A2) [failures divergences model] | 548 | 1011 | true |
SpecA3 is deadlock free (A3) [failures divergences model] | 2 | 25 | true |
Movement is divergence free (A4) [failures divergences model] | 81848 | 167682 | true |
SpecA5 is deadlock free (A5) [failures divergences model] | 77 | 264 | true |
SpecB3 is deadlock free (B3) [failures divergences model] | 3 | 7 | true |
The compilation and verification statistics were obtained by runnning FDR4 on Manjaro Linux on a Laptop with a Intel(R) Core(TM) i7-4700MQ CPU @ 2.40GHz
processor and 32GB of RAM. ↩
The compilation was aborted when memory usage increased beyond 30GB because reaching 32GB crashes the system and requires reboot. ↩
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500
University of York legal statements