| Deterministic
transitions |
|
|
|
|
|
|
|
|
|
|
|
|
| • | Do
the same conditions allow for non- |
||||||||||
| deterministic
transitions? |
|||||||||||
| • | Inconsistencies
were found earlier (in an earlier |
||||||||||
| version
of TCAS) by other methods [Heimdahl
and |
|||||||||||
| Leveson] |
|||||||||||
| – | Identical
conditions allowed transitions from Sensitivity |
||||||||||
| Level
4 to SL 2 or to SL 5 |
|||||||||||
| • | Our
formulae checked for all possible non- |
||||||||||
| determinism;
we found this case, too |
|||||||||||
