Projekter pr. år
Abstract
We introduce Randomized Reachability Analysis – an efficient and highly scalable method for detection of “rare event” states, such as errors. Due to the under-approximate nature of the method, it excels at quick falsification of models and can greatly improve the model-based development process: using lightweight randomized methods early in the development for the discovery of bugs, followed by expensive symbolic verification only at the very end. We show the scalability of our method on a number of Timed Automata and Stopwatch Automata models of varying sizes and origin. Among them, we revisit the schedulability problem from the Herschel-Planck industrial case study, where our new method finds the deadline violation three orders of magnitude faster: some cases could previously be analyzed by statistical model checking (SMC) in 23 h and can now be checked in 23 s. Moreover, a deadline violation is discovered in a number of cases that where previously intractable. We have implemented the Randomized Reachability Analysis – and made it available – in the tool Uppaal.
Originalsprog | Engelsk |
---|---|
Titel | Formal Methods for Industrial Critical Systems : 26th International Conference, FMICS 2021, Proceedings |
Redaktører | Alberto Lluch Lafuente, Anastasia Mavridou |
Antal sider | 18 |
Forlag | Springer Science+Business Media |
Publikationsdato | 2021 |
Sider | 149-166 |
ISBN (Trykt) | 9783030852474 |
DOI | |
Status | Udgivet - 2021 |
Begivenhed | 26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021 - Virtual, Online Varighed: 24 aug. 2021 → 26 aug. 2021 |
Konference
Konference | 26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021 |
---|---|
By | Virtual, Online |
Periode | 24/08/2021 → 26/08/2021 |
Navn | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Vol/bind | 12863 LNCS |
ISSN | 0302-9743 |
Bibliografisk note
Funding Information:Supported by the ERC Advanced Grant Project: LASSO: Learning, Analysis, Synthesis and Optimization of Cyber-Physical Systems, and by the Villum Investigator project S4OS: Synthesis of Safe, Small, Secure and Optimal Strategies for Cyber-Physical Systems.
Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
Fingeraftryk
Dyk ned i forskningsemnerne om 'Randomized Reachability Analysis in Uppaal: Fast Error Detection in Timed Systems'. Sammen danner de et unikt fingeraftryk.Projekter
- 1 Igangværende
-
S4OS: SCALABLE ANALYSIS OF SAFE, SMALL AND SECURE STRATEGIES FOR CYBER-PHYSICAL SYSTEMS
01/01/2021 → 31/12/2027
Projekter: Projekt › Forskning
-
Efficient Model Checking: The Power of Randomness
Kiviriga, A., 2023, Aalborg Universitetsforlag. 153 s.Publikation: Ph.d.-afhandling
Åben adgangFil98 Downloads (Pure) -
Randomized reachability analysis in UPPAAL: fast error detection in timed systems*
Kiviriga, A., Larsen, K. G. & Nyman, U., 17 nov. 2022, I: International Journal on Software Tools for Technology Transfer. 24, 6, s. 1025-1042 18 s.Publikation: Bidrag til tidsskrift › Konferenceartikel i tidsskrift › Forskning › peer review
Åben adgangFil1 Citationer (Scopus)27 Downloads (Pure)