Randomized Refinement Checking of Timed I/O Automata

To combat the state-space explosion problem and ease system development, we present a new refinement checking (falsification) method for Timed I/O Automata based on random walks. Our memory-less heuristics Random Enabled Transition (RET) and Random Channel First (RCF) provide efficient and highly scalable methods for counterexample detection. Both RET and RCF operate on concrete states and are relieved from expensive computations of symbolic abstractions. We compare the most promising variants of RET and RCF heuristics to existing symbolic refinement verification of the Ecdar tool. The results show that as the size of the system increases our heuristics are significantly less prone to exponential increase of time required by Ecdar to detect violations: in very large systems both “wide” and “narrow” violations are found up to 600 times faster and for extremely large systems when Ecdar timeouts, our heuristics are successful in finding violations.