Randomized reachability analysis in UPPAAL: fast error detection in timed systems*

Research output: Contribution to journalConference article in JournalResearchpeer-review

1 Citation (Scopus)


Randomized reachability analysis is an efficient method for detection of safety violations. 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 in 23 h and can now be checked in 23 s. Moreover, a deadline violation is discovered in a number of cases that were previously intractable. We have implemented the Randomized reachability analysis—and made it available—in the tool UPPAAL. Finally, we provide an evaluation of the strengths and weaknesses of Random reachability analysis exploring exactly which types of model features hamper method’s efficiency.
Original languageEnglish
JournalInternational Journal on Software Tools for Technology Transfer
Issue number6
Pages (from-to)1025-1042
Number of pages18
Publication statusPublished - 17 Nov 2022
Event26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021 - Virtual, Online
Duration: 24 Aug 202126 Aug 2021


Conference26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021
CityVirtual, Online


  • Model-checking
  • Randomized
  • Schedulability analysis
  • State space explosion
  • Stopwatch automata
  • Timed automata


Dive into the research topics of 'Randomized reachability analysis in UPPAAL: fast error detection in timed systems*'. Together they form a unique fingerprint.
  • Randomized Reachability Analysis in Uppaal: Fast Error Detection in Timed Systems

    Kiviriga, A., Larsen, K. G. & Nyman, U., 2021, Formal Methods for Industrial Critical Systems : 26th International Conference, FMICS 2021, Proceedings. Lluch Lafuente, A. & Mavridou, A. (eds.). Springer Science+Business Media, p. 149-166 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 12863 LNCS).

    Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

    Open Access
    51 Downloads (Pure)

Cite this