- Room No: G.2.06
- Telephone: +64 7 838 4466
- Extension: 6011
- Facsimile: +64 7 838 4155
BCMS Honours Topic: "Compositional nonblocking verification with Always Enabled Events."
I am extending the compositional nonblocking verification rules currently implemented in Waters by using Always Enabled Events. Waters is a model checker, used to model safety-critical reactive systems. Nonblocking ensures the system has no livelocks or deadlocks. Compositional verification is an effective way to check nonblocking for large systems that avoids state space explosions. Always Enabled Events are events that are not disabled in any automata other than the one being simplified. I have seen they have interesting properties when combined with some simplification rules. So I am extending the current implementation of these rules in Waters to include Always Enabled Events, writing new heuristics to take advantage of this and testing to see any increases in performance.