Randomized Refinement Checking of Timed I/O Automata

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

44 Downloads (Pure)


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.
TitelProceedings of SETTA 2020 : Dependable Software Engineering. Theories, Tools, and Applications
RedaktørerJun Pang, Lijun Zhang
Antal sider19
Publikationsdato9 nov. 2020
ISBN (Trykt)978-3-030-62821-5
ISBN (Elektronisk)978-3-030-62822-2
StatusUdgivet - 9 nov. 2020
BegivenhedInternational Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2020) - Guangzhou, Kina
Varighed: 24 nov. 202027 nov. 2020


KonferenceInternational Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2020)
NavnLecture Notes in Computer Science

Fingeraftryk Dyk ned i forskningsemnerne om 'Randomized Refinement Checking of Timed I/O Automata'. Sammen danner de et unikt fingeraftryk.