Department of Computer Science

Chemical Detector

  1. Introduction
  2. Version 1.0
  3. Version 2.0
  4. Version 3.0
  5. Timed Properties

Introduction

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:

1) The machine Detecting should be nondeterministic.
assert not Detecting_O :[deterministic]
2) Every command should lead to an event turn or two calls to operations incr or decr.
Commands = cd?x -> (|~|e: {|turn,incrCall,decrCall|} @ e -> Commands)
3) Initially the model is prepared to detect a gas and flash the light green, in any order.
Init = light.green -> SKIP ||| gas -> SKIP
4) Whenever a gas is detected, a light should flash. When the light flashes red, a siren must sound and a flag must be dropped. At most to gas detections can occur before the light must flash.
GasLight = let
  T = (
    gas -> SKIP
    |||
    (
      light.red -> siren -> flag -> SKIP
      |~|
      light.green -> SKIP
      |~|
      light.amber -> SKIP
    )
  ); T
within
  Init; T
5) The chemical detector is always ready to accept a command.
assert ChemicalDetectorSoftware_O [|{|gas,light|}|] STOP :[deadlock free]
6) The chemical detector is always ready to accept a gas read.
assert ChemicalDetectorSoftware_O [|{|cd|}|] STOP :[deadlock free]
7) Gas detection and commands should not interfere with each other.
assert (Commands ||| GasLight) [F= ChemicalDetectorSoftware_O\{|incrRet, decrRet|}
8-13) Other requirements are basic properties such as deadlock and livelock freedom.
assert ChemicalDetectorSoftware_O :[deadlock free]
assert ChemicalDetectorSoftware_O :[divergence free]

ChemicalDetector 1.0 (download)

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.

Model

Analysis

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

ChemicalDetector 2.0 (download)

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.

Model

Analysis

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

ChemicalDetector 3.0 (download)

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).

Model

Analysis

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

Timed Properties

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.

tock-CSP

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.

Deadlines

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.

Timelocks

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.

System Requirements

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.

T1) Whenever a gas is detected, a light state change should be accepted within at most 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)
T2) Whenever a gas reading is received, the light state should change within at most 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
T3) Whenever the siren is triggered, the flag should be dropped within 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|}
T4) Whenever a dangerous gas is detected, the flag should be dropped within 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"|})
T5) Whenever a command is issued to turn 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
T6) The system accepts a gas reading every 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})

Core Time Checks

TC1) Every state can be reached.

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"|}
TC2) Every state that could be reached without consideration for time can also be reached when considering time.
assert ChemicalDetectorSoftware [T= TimedChemicalDetectorSoftware \{tock}
TC3) The system does not initiate an infinite number of events within a finite time.
assert ChemicalDetectorSoftware |\ union(ExternalEvents,{tock}) :[divergence free]
TC4) The system does not time lock.
assert RUN({tock}) ||| CHAOS(ExternalEvents) [FD= ChemicalDetectorSoftware |\ union(ExternalEvents,{tock})
TC5) The system does not live lock.
assert ChemicalDetectorSoftware :[divergence free]

Analysis

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.

Model revision 0

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.

Requirement T1

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.

Requirement T2

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.

Requirement T3

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.

Requirement T4

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.

Summary of analysis
Requirement Result
T1 fail
T2 fail
T3 fail
T4 fail
T5 fail
TC1 pass
TC2 pass
TC3 pass
TC4 pass
TC5 pass

Model revision 1

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.

Requirement T1

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.

Requirement T2

Assertion: GasLightWithinStrict(t) [T= ChemicalDetectorSoftware

Conclusion: Same as in model revision 0.

Requirement T3

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
Requirement T4

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 T5

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 T6

Assertion: assert RUN({tock}) ||| CHAOS(ExternalEvents) [FD= SystemT5 |\ union(ExternalEvents,{tock})

Conclusion: Passes for various t values tried.

Summary of analysis
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

Model revision 2

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.

Requirement T1

Same as before.

Requirement T2

Same as before.

Requirement T3
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.

Requirement T4

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 T5

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.

Summary of analysis
Requirement Result
T1 ? sometimes
T2 ?
T3 ?
T4 ?
T5 ?
TC1 pass
TC2 pass
TC3 pass
TC4 pass
TC5 pass

Summary

Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500
University of York legal statements