Chris Johnson, Index
Leveson's Completeness Criteria
background image



Robustness:
every state has a transition defined for every possible input.

Non-determinism:
only 1 transition is possible from a state for each input.

Value and Timing assumptions:
- what triggers can be produced from the environment?
- what ranges must trigger variables fall within?
- what are the real-time requirements...
- specify bounds for responses to input (timeouts)




forward