Design Criteria
Efficiency
- Simple model: networks of timed automata with integers and drifting clocks
- Simple requirements: safety, (bounded) liveness
- On-the-fly checking
Ease of usage
- Graphical interface
- Diagnostic traces (shortest)
- Graphical simulation