Randomized Refinement Checking of Timed I/O Automata

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

44 Downloads (Pure)

Abstrakt

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

Konference

KonferenceInternational Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2020)
LandKina
ByGuangzhou
Periode24/11/202027/11/2020
NavnLecture Notes in Computer Science
Vol/bind12153
ISSN0302-9743

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

Citationsformater