Chris Johnson, Index
Leveson's Completeness Criteria
all specified states can be reached from initial state.
desired recurrent behaviour must execute for at least one cycle and be bounded by exit condition.
output commands should wherever possible be reversible and those which are not must be carefully controlled.
all possible preemption events must be considered for any non-atomic transactions.
- Again more complexity here...