Chris Johnson, Index
Leveson's Completeness Criteria
background image

Reachability:
all specified states can be reached from initial state.

Recurrent behaviour:
desired recurrent behaviour must execute for at least one cycle and be bounded by exit condition.

Reversibility:
output commands should wherever possible be reversible and those which are not must be carefully controlled.

Preemption:
all possible preemption events must be considered for any non-atomic transactions.
forward