This page documents the development of the chemical detector. So far, it consists of three chapters: Version 1.0 presents the initial model of the chemical detector, initial property verifications, and mistakes detected; Version 2.0 presents an updated version of the model based on the results found in the previous chapter, and repeats the verification; and Version 3.0 presents the latest version of the model, again, based on the results of from Version 2.0. Finally, Timed Properties considers specification and analysis of timed properties. An autonomous version of the chemical detector is presented as a separate case study.
As a basis for verification, we define a few requirements for the chemical detector and encode them as CSP processes:
assert not Detecting_O :[deterministic]
turn
or two calls to operations incr
or decr
.Commands = cd?x -> (|~|e: {|turn,incrCall,decrCall|} @ e -> Commands)
Init = light.green -> SKIP ||| gas -> SKIP
GasLight = let
T = (
gas -> SKIP
|||
(
light.red -> siren -> flag -> SKIP
|~|
light.green -> SKIP
|~|
light.amber -> SKIP
)
); T
within
Init; T
assert ChemicalDetectorSoftware_O [|{|gas,light|}|] STOP :[deadlock free]
assert ChemicalDetectorSoftware_O [|{|cd|}|] STOP :[deadlock free]
assert (Commands ||| GasLight) [F= ChemicalDetectorSoftware_O\{|incrRet, decrRet|}
assert ChemicalDetectorSoftware_O :[deadlock free]
assert ChemicalDetectorSoftware_O :[divergence free]
The intention in this model is to abstract the algorithm for analysing and detecting gases using non-determinism, therefore requirement 1 should be valid. The analysis shows that this requirement is not valid (that is, it shows that Detecting is deterministic) indicating a mistake in the model. We identify the source of this problem as the usage of the detect
events as triggers and not actions in the transitions of the machine Detecting. This mistake is corrected in the model presented in the next Chapter.
Requirement | Result |
---|---|
1. Detecting is nondeterministic | false |
2. Commands leads to turn, incr or dect | true |
3. Definition of Init | n/a |
4. Definition of GasLight | n/a |
5. Always ready to accept a command | true |
6. Always willing to accept gas read | true |
7. Gas detection and commands noninterference | true |
8. MainComputer deadlock and divergence free | true |
9. Moving is deterministic, and deadlock and divergence free | true |
10. Detecting is deadlock and divergence free | true |
11. Microcontroller is deadlock and divergence free | true |
12. Signalling is deadlock and divergence free | true |
13. ChemicalDetectorSoftware is deadlock and divergence free | true |
This models fixes the issue with the determinism of Detecting by moving the events from the triggers to the transition actions. This time, the analysis shows that requirement 1 is valid, but the model no longer satisfies requirements 6 (deadlock freedom of gas detection) and 7 (non-interference of gas detection and commands).
The verification of requirement 6 shows that the model can deadlock after a trace [light.green, gas]
, which suggests verifying extensions of this trace, for example [light.green, gas, light.red] and [light.green, gas, light.green]. The verification of these traces shows that [light.green, gas, light.green] is in fact not a trace of the model. A detailed evaluation the model based on this trace
leads to the observation that the state Waiting
of machine Signalling
is not prepared to accept the eventdetect.innocuous
. The evaluation of the model also reveals missing transitions in the states AnomalousGas and DangerousGas. The missing transitions are added to the model in the next Chapter.
Requirement | Result |
---|---|
1. Detecting is nondeterministic | true |
2. Commands leads to turn, incr or dect | true |
3. Definition of Init | n/a |
4. Definition of GasLight | n/a |
5. Always ready to accept a command | true |
6. Always willing to accept gas read | false |
7. Gas detection and commands noninterference | false |
8. MainComputer is deadlock and divergence free | true |
9. Moving is deterministic, and deadlock and divergence free | true |
10. Detecting is deadlock and divergence free | true |
11. Microcontroller is deadlock and divergence free | true |
12. Signalling is deadlock and divergence free | true |
13. ChemicalDetectorSoftware is deadlock and divergence free | true |
In order to avoid the deadlock introduced in the previous chapter, we add self transitions to each state in Signalling
to accept the missing event. Adding the missing transitions and repeating the analysis on this new model now yields the expected results. The model is nondeterministic (requirement 1) and divergence free (basic property); the model as a whole and its specific behaviours (gas detection and commands) are dealock free (basic properties and requirements 5 and 6). The model refines the abstract specification of the desired behaviour (requirement 7).
Requirement | Result |
---|---|
1. Detecting is nondeterministic | true |
2. Commands leads to turn, incr or dect | true |
3. Definition of Init | n/a |
4. Definition of GasLight | n/a |
5. Always ready to accept a command | true |
6. Always willing to accept gas read | true |
7. Gas detection and commands noninterference | true |
8. MainComputer is deadlock and divergence free | true |
9. Moving is deterministic, and deadlock and divergence free | true |
10. Detecting is deadlock and divergence free | true |
11. Microcontroller is deadlock and divergence free | true |
12. Signalling is deadlock and divergence free | true |
13. ChemicalDetectorSoftware is deadlock and divergence free | true |
14. Gas detection leads to light change within t time units. |
false |
In this section we discuss the specification and analysis of timed properties related to the Chemical Detector system. In the section on tock-CSP we discuss how timed properties can be specified using tock-CSP
, and how checks can be performed using appropriate assertions. In the Requirements section we list a number of timed requirements and their respective CSP encoding. Finally at the end of the section we present the result of analysing the properties on the Chemical Detector system.
Timed properties can be specified using tock-CSP
processes. Below we use the syntax of Timed CSP
, with additional constructs to capture deadlines, taking into account that the process is translated to tock-CSP
using the facilities provided by FDR within a Timed block.
A Deadline(P,d)
of d
time units is specified below as allowing up to d
occurrences of the tock
event, after which the process P
is not allowed to consume any further time, achieved by refusing tock
.
channel finished
Deadline(P, t) = ((P ; finished -> SKIP) [|{tock, finished}|] (Wait(t) /\ finished->SKIP)) \ {finished}
The process P
initially synchronizes with Wait(t)
that allows t
units of time to pass. If P
terminates before Wait(t)
, then the internal event finished
interrupts the Wait(t)
following the principle of maximal progress where internal events are executed for as long as possible before time passes (encoded in FDR using the prioritisation function timed_priority
, which prioritises internal events over tock
).
Similarly we define a simpler version EDeadline(e)
for a single event e
.
EDeadline(e,d) = (Wait(d) ; STOP) /\ (e -> SKIP)
In addition, we define the following auxiliary processes that allow other events to take place while waiting on a deadline.
AnyOther(e) = CHAOS(Events) [|{e}|> SKIP
ADeadline(e,d) = (CHAOS(Events) [| {tock} |] Wait(d)) [|{e}|> SKIP
The process AnyOther(e)
allows any event to take place nondeterministically, and if e
is chosen, then the process terminates. The process ADeadline(e,d)
behaves in a similar way, except it only allows events to take place within d
time units.
Failure to meet a deadline results in a timed deadlock, which, in general, can be identified with a refinement check, as we describe below.
Given a tock-CSP
process P
, and a known set ExternalEvents
containing those events that can be observed by the environment, then following Roscoe’s work, the assertion is defined as follows:
assert RUN({tock}) ||| CHAOS(ExternalEvents) [FD= P |\ union(ExternalEvents,{tock})
It must be the case that tock
is always offered, and any event in the set ExternalEvents
may or may not be offered by P
. A timed deadlock eventually refuses tock
even if it is willing to accept other events.
We identify the set of ExternalEvents
for the Chemical Detector as gas
and cd
: ExternalEvents = {|gas,cd|}
. Below we list the system requirements and their specification as tock-CSP
processes.
t
time units, and initially the green light status should be accepted within t
time units as well. This includes light state changes between the same colour. Furthermore, any amount of time can elapse while accepting the siren
and flag
events.We encode the specification for this requirement using the process GasLightWithin(t)
,
GasLightWithin(t) = let
InitT = (EDeadline(light.green,t) ; SKIP) ||| gas -> SKIP
T = (
gas -> SKIP
|||
(
EDeadline(light.red,t) ; siren -> flag -> SKIP
|~|
EDeadline(light.green,t) ; SKIP
|~|
EDeadline(light.amber,t) ; SKIP
)
); T
within
timed_priority((InitT; T) ||| CHAOS(diff(Events,{|light,gas,siren,flag|}))
where every other event other than gas
, light
, siren
and flag
is allowed to happen independently, encoded using CHAOS(E)
, the process that does not livelock and offers a non-deterministic choice over the events in the set of all Events
except for the events we control light
, gas
, siren
and flag
. We can then check that the system does not violate this property for a given time t
using the following assertion:
assert GasLightWithin(t) [FD= ChemicalDetectorSoftware
Alternatively, this can be checked in a different way by considering the process GasLightAt(t)
, which allows the light
to change after a nondeterministic minimum time interval from 0
to t
time units.
NWait(e,t) = |~| n : {0..t} @ (WAIT(n) ; e -> SKIP)
GasLightAt(t) =
let
InitT = (NWait(light.green,t) ; SKIP) ||| gas -> SKIP
T = (
gas -> SKIP
|||
(
NWait(light.red,t) ; siren -> flag -> SKIP
[]
NWait(light.green,t)
[]
NWait(light.amber,t)
)
); T
within
timed_priority(InitT; T)
We then compose the original system ChemicalDetectorSoftware
with GasLightAt(t)
to check whether the system allows light
to happen at least t
time units after the occurrence of gas
.
SystemGasLightAt(t) = timed_priority((
ChemicalDetectorSoftware
[| {|light,gas,siren,flag|} |]
GasLightAt(t)) |\ union(ExternalEvents,{tock}))
Then check for timed deadlocks of the system SystemGasLightAt
:
assert RUN({tock}) ||| CHAOS(ExternalEvents) [FD= SystemGasLightAt(t)
t
time units.We observe that this requirement is stronger than T1 as it applies irrespective of the time taken to accept siren
or flag
.
GasLightWithinStrict(t) = let
InitT = (EDeadline(light.green,t) ; SKIP) ||| gas -> SKIP
T = (
gas -> SKIP
|||
(
EDeadline(light.red,t) ; SKIP
|~|
EDeadline(light.green,t) ; SKIP
|~|
EDeadline(light.amber,t) ; SKIP
)
); T
OtherEvents = CHAOS(union(diff(Events,{|light,gas,siren,flag|}),{tock}))
within
timed_priority((InitT; T) ||| OtherEvents)
In this case, because we do not specify when siren
and flag
should happen, the verification has to be performed in the traces model:
assert GasLightWithinStrict(t) [T ChemicalDetectorSoftware
t
time units.SirenToFlagWithin(t) = let
SomeGas = gas -> SKIP
T = SomeGas ; (SomeGas ||| (siren -> Deadline(flag -> SKIP,t) |~| SKIP)) ; T
within
timed_priority (T ||| CHAOS(diff(Events,{|siren,flag,gas|})))
assert SirenToFlagWithin(t) [FD= ChemicalDetectorSoftware \{|light|}
t
time units.We define the following specification, which allows any other event to take place followed by Signalling_entered."Signalling_DangerousGas"
(that signals the state has been asked to enter), followed by a deadline on event flag
, while allowing any other event to take place.
DangerousDropFlagWithin(t) = let
DangerousFlag = AnyOther(Signalling_entered."DangerousGas") -> ADeadline(flag,t) ; DangerousFlag
within
timed_priority(DangerousFlag)
We then check the property using the following assertion, where we hide all InternalEvents
in the ChemicalDetectorSoftware_StatesView
apart from Signalling_entered."DangerousGas"
.
assert DangerousDropFlagWithin(t) [FD= ChemicalDetectorSoftware_StatesView
\ diff(InternalEvents,{|Signalling_entered."DangerousGas"|})
right
, left
or move back
, a corresponding turn
event must happen within t
time units.CommandWithin(t) =
let
Commands = (cd?{slower,faster} -> SKIP
[]
cd?{back,left,right} -> Deadline(|~| e : {|turn|} @ e -> SKIP,t)) ; Commands
within
timed_priority(Commands ||| CHAOS(diff(Events,{|cd,turn|})))
assert CommandWithin(t) [T= ChemicalDetectorSoftware
t
time units.GasReadingEvery(t) =
let
GasReading = gas -> SKIP ; Wait(t) ; GasReading
within
timed_priority(GasReading)
SystemT5 = ChemicalDetectorSoftware [| {|gas|} |] GasReadingEvery(t)
assert RUN({tock}) ||| CHAOS(ExternalEvents) [FD= SystemT5 |\ union(ExternalEvents,{tock})
Note that to check this property need to make the internal events entered
visible.
assert not STOP [T= ChemicalDetectorSoftware |\ {|Signalling_entered."Waiting"|}
assert not STOP [T= ChemicalDetectorSoftware |\ {|Signalling_entered."AnomalousGas"|}
assert not STOP [T= ChemicalDetectorSoftware |\ {|Signalling_entered."DangerousGas"|}
assert not STOP [T= ChemicalDetectorSoftware |\ {|Detecting_entered."CleanAir"|}
assert not STOP [T= ChemicalDetectorSoftware |\ {|Detecting_entered."GasPresent"|}
assert not STOP [T= ChemicalDetectorSoftware |\ {|Moving_entered."Waiting"|}
assert ChemicalDetectorSoftware [T= TimedChemicalDetectorSoftware \{tock}
assert ChemicalDetectorSoftware |\ union(ExternalEvents,{tock}) :[divergence free]
assert RUN({tock}) ||| CHAOS(ExternalEvents) [FD= ChemicalDetectorSoftware |\ union(ExternalEvents,{tock})
assert ChemicalDetectorSoftware :[divergence free]
Below we discuss the results of analysing the Chemical Detector system, starting with the original model of the system (in Model revision 0). Following problems checking some of the requirements we proceed by considering revised versions of the model that can meet those requirements under certain assumptions.
This is the original model of the Chemical Detector, with no deadlines specified on any of the events. Below we show the Signalling
state-machine.
Assertion: assert GasLightWithin(t) [FD= ChemicalDetectorSoftware
Value of t |
Result |
---|---|
0 | false |
1 | false |
2 | false |
3 | false |
Conclusion: System cannot guarantee that the light will change within t
because send light
is not guaranteed to complete within a certain fixed amount of time.
Assertion: assert RUN({tock}) ||| CHAOS(ExternalEvents) [FD= SystemGasLightAt(t)
Value of t |
Value of dL |
Result |
---|---|---|
0 | 1 | false |
1 | 1 | false |
2 | 1 | false |
3 | 1 | false |
Conclusion: System cannot guarantee that the light will change within t
because send light
is not guaranteed to complete within a certain fixed amount of time.
Assertion: GasLightWithinStrict(t) [T= ChemicalDetectorSoftware
Value of t |
Value of flagTime |
Result |
---|---|---|
0 | 0 | false |
1 | 0 | false |
2 | 0 | false |
3 | 0 | false |
Conclusion: Because there is no assumption on when send siren
and send flag
must happen, it is not possible to satisfy Requirement T1.
Assertion: SirenToFlagWithin(t) [T= ChemicalDetectorSoftware
Value of t |
Value of flagTime |
Result |
---|---|---|
0 | 0 | false |
1 | 0 | false |
2 | 1 | false |
3 | 2 | false |
Conclusion: Because there is no assumption on when send flag
must happen, it is not possible to guarantee Requirement T2.
Assertion:
assert DangerousDropFlagWithin(t) [FD= ChemicalDetectorSoftware_StatesView
\ diff(InternalEvents,{|Signalling_entered."DangerousGas"|})
Conclusion: Not possible to satisfy requirement for any t
because there is no assumption on when send siren
and send flag
must happen.
Requirement | Result |
---|---|
T1 | fail |
T2 | fail |
T3 | fail |
T4 | fail |
T5 | fail |
TC1 | pass |
TC2 | pass |
TC3 | pass |
TC4 | pass |
TC5 | pass |
To bound the time taken to instruct the platform to change the status of the light, in this model revision the we add deadlines (<{dL}
) to every send light
statement in the state-machine Signalling.
Assertion: assert GasLightWithin(t) [FD= ChemicalDetectorSoftware
Value of t |
Value of dL |
Result |
---|---|---|
0 | 1 | false |
1 | 1 | true |
2 | 1 | true |
3 | 1 | true |
Conclusion: System can guarantee that light will change for t >= 1
.
Assertion: assert RUN({tock}) ||| CHAOS(ExternalEvents) [FD= SystemGasLightAt(t)
Value of t |
Value of dL |
Result |
---|---|---|
0 | 1 | true |
1 | 1 | true |
2 | 1 | false |
3 | 1 | false |
Conclusion: System is not guaranteed to be able to change the light within the interval 0
to dL+1
, but for t <= dL
it is.
Note: It takes significantly longer to check this assertion than the first one.
Assertion: GasLightWithinStrict(t) [T= ChemicalDetectorSoftware
Conclusion: Same as in model revision 0.
Assertion: SirenToFlagWithin(t) [FD= ChemicalDetectorSoftware \{|light|}
Value of t |
Value of dF |
Result |
---|---|---|
0 | 1 | false |
1 | 1 | false |
0 | 2 | false |
1 | 2 | false |
Assertion:
assert DangerousDropFlagWithin(t) [FD= ChemicalDetectorSoftware_StatesView
\ diff(InternalEvents,{|Signalling_entered."DangerousGas"|})
Conclusion: Not possible to satisfy requirement for any t
because there is no assumption on when send siren
and send flag
must happen.
Assertion: assert CommandWithin(t) [T= ChemicalDetectorSoftware
Conclusion: Not possible to satisfy requirement for any t
because there is no assumption on when send turn
must happen.
Assertion: assert RUN({tock}) ||| CHAOS(ExternalEvents) [FD= SystemT5 |\ union(ExternalEvents,{tock})
Conclusion: Passes for various t
values tried.
Requirement | Result |
---|---|
T1 | satisfiable sometimes |
T2 | fail |
T3 | fail |
T4 | fail |
T5 | fail |
T6 | pass |
TC1 | pass |
TC2 | pass |
TC3 | pass |
TC4 | pass |
TC5 | pass |
To bound the time taken to instruct the platform to drop the flag we add a deadline (<{dF}
) to send flag
on state-machine Signalling.
Same as before.
Same as before.
Value of t |
Value of dF |
Value of flagTime |
Result |
---|---|---|---|
0 | 0 | 0 | pass |
1 | 1 | 0 | pass |
1 | 0 | 1 | pass |
1 | 2 | 0 | fail |
2 | 2 | 0 | pass |
Conclusion: Provided flagTime + dF <= t
, then the send flag
happens within t
time units after the siren
is activated.
Assertion:
assert DangerousDropFlagWithin(t) [FD= ChemicalDetectorSoftware_StatesView
\ diff(InternalEvents,{|Signalling_entered."DangerousGas"|})
Conclusion: Not possible to satisfy requirement for any t
because there is no assumption on when send siren
and send flag
must happen.
Assertion: assert CommandWithin(t) [T= ChemicalDetectorSoftware
Conclusion: Not possible to satisfy requirement for any t
because there is no assumption on when send turn
must happen.
Requirement | Result |
---|---|
T1 | ? sometimes |
T2 | ? |
T3 | ? |
T4 | ? |
T5 | ? |
TC1 | pass |
TC2 | pass |
TC3 | pass |
TC4 | pass |
TC5 | pass |
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500
University of York legal statements