Skip to main content
Erschienen in:

17.11.2022 | General

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

verfasst von: Andrej Kiviriga, Kim Guldstrand Larsen, Ulrik Nyman

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 6/2022

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literatur
1.
Zurück zum Zitat Kiviriga, A., Larsen, K.G., Nyman, U.: Randomized Refinement Checking of Timed I/O Automata. In: Pang, J., Zhang, L. (eds.) Dependable Software Engineering. Theories, Tools, and Applications, pp. 70–88. Springer, Cham (2020) Kiviriga, A., Larsen, K.G., Nyman, U.: Randomized Refinement Checking of Timed I/O Automata. In: Pang, J., Zhang, L. (eds.) Dependable Software Engineering. Theories, Tools, and Applications, pp. 70–88. Springer, Cham (2020)
2.
Zurück zum Zitat Grosu, R., Smolka, S.A.: Monte Carlo Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 271–286. Springer, Berlin, Heidelberg (2005)CrossRef Grosu, R., Smolka, S.A.: Monte Carlo Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 271–286. Springer, Berlin, Heidelberg (2005)CrossRef
3.
Zurück zum Zitat Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Formal Methods for the Design of Real-time Systems, pp. 200–236. Springer (2004) Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Formal Methods for the Design of Real-time Systems, pp. 200–236. Springer (2004)
5.
Zurück zum Zitat Burns, A.: Preemptive Priority-Based Scheduling: An Appropriate Engineering Approach, pp. 225–248. Prentice-Hall, Inc., Hoboken (1995) Burns, A.: Preemptive Priority-Based Scheduling: An Appropriate Engineering Approach, pp. 225–248. Prentice-Hall, Inc., Hoboken (1995)
9.
Zurück zum Zitat Mikučionis, M., Larsen, K.G., Rasmussen, J.I., Nielsen, B., Skou, A., Palm, S.U., Pedersen, J.S., Hougaard, P.: Schedulability analysis using uppaal: Herschel–Planck case study. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification, and Validation, pp. 175–190. Springer, Berlin, Heidelberg (2010)CrossRef Mikučionis, M., Larsen, K.G., Rasmussen, J.I., Nielsen, B., Skou, A., Palm, S.U., Pedersen, J.S., Hougaard, P.: Schedulability analysis using uppaal: Herschel–Planck case study. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification, and Validation, pp. 175–190. Springer, Berlin, Heidelberg (2010)CrossRef
10.
Zurück zum Zitat David, A., Illum, J., Larsen, K. G., Skou, A.: Model-based framework for schedulability analysis using uppaal 4.1. Model-Based Design Embedded Syst. 1(1), 93–119 (2009)CrossRef David, A., Illum, J., Larsen, K. G., Skou, A.: Model-based framework for schedulability analysis using uppaal 4.1. Model-Based Design Embedded Syst. 1(1), 93–119 (2009)CrossRef
11.
Zurück zum Zitat David, A., Larsen, K.G., Legay, A., Mikučionis, M.: Schedulability of Herschel–Planck Revisited Using Statistical Model Checking. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, pp. 293–307. Springer, Berlin, Heidelberg (2012) David, A., Larsen, K.G., Legay, A., Mikučionis, M.: Schedulability of Herschel–Planck Revisited Using Statistical Model Checking. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, pp. 293–307. Springer, Berlin, Heidelberg (2012)
12.
Zurück zum Zitat Palm, S.: Herschel-planck acc asw: sizing, timing and schedulability analysis. Tech. rep., Terma A/S, Technical report (2006) Palm, S.: Herschel-planck acc asw: sizing, timing and schedulability analysis. Tech. rep., Terma A/S, Technical report (2006)
13.
Zurück zum Zitat Cassez, F., Larsen, K.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000–Concurrency Theory, pp. 138–152. Springer, Berlin, Heidelberg (2000)CrossRef Cassez, F., Larsen, K.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000–Concurrency Theory, pp. 138–152. Springer, Berlin, Heidelberg (2000)CrossRef
15.
Zurück zum Zitat Sen, K., Viswanathan, M., Agha, G.: Statistical Model Checking of Black-Box Probabilistic Systems. In: Alur, R., Peled, D.A. (eds.) Computer Aided Verification, pp. 202–215. Springer, Berlin, Heidelberg (2004) Sen, K., Viswanathan, M., Agha, G.: Statistical Model Checking of Black-Box Probabilistic Systems. In: Alur, R., Peled, D.A. (eds.) Computer Aided Verification, pp. 202–215. Springer, Berlin, Heidelberg (2004)
16.
Zurück zum Zitat Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: An overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) Runtime Verification, pp. 122–135. Springer, Berlin, Heidelberg (2010) Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: An overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) Runtime Verification, pp. 122–135. Springer, Berlin, Heidelberg (2010)
17.
Zurück zum Zitat David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Software Tools Technol. Transf. 17(4), 397–415 (2015)CrossRef David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Software Tools Technol. Transf. 17(4), 397–415 (2015)CrossRef
18.
Zurück zum Zitat Alur, R., Dill, D.: The theory of timed automata. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) Real-Time: Theory in Practice, pp. 45–73. Springer, Berlin, Heidelberg (1992)CrossRef Alur, R., Dill, D.: The theory of timed automata. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) Real-Time: Theory in Practice, pp. 45–73. Springer, Berlin, Heidelberg (1992)CrossRef
19.
Zurück zum Zitat Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Priced timed automata: algorithms and applications. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) Formal Methods Comp. Obj., pp. 162–182. Springer, Berlin, Heidelberg (2005)CrossRef Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Priced timed automata: algorithms and applications. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) Formal Methods Comp. Obj., pp. 162–182. Springer, Berlin, Heidelberg (2005)CrossRef
20.
Zurück zum Zitat Larsen, K., Peled, D., Sedwards, S.: Memory-Efficient Tactics for Randomized LTL Model Checking. In: Paskevich, A., Wies, T. (eds.) Verified Software. Theories, Tools, and Experiments, pp. 152–169. Springer, Cham (2017) Larsen, K., Peled, D., Sedwards, S.: Memory-Efficient Tactics for Randomized LTL Model Checking. In: Paskevich, A., Wies, T. (eds.) Verified Software. Theories, Tools, and Experiments, pp. 152–169. Springer, Cham (2017)
23.
Zurück zum Zitat Martins Gomes, R., Baunach, M., Batista Ribeiro, L.: MCSmartOS: A Dependable OS for Compositional Embedded Systems. (2017). FoE-Tag des Field of Expertise “Information, Communication and Computing” ; Conference date: 28-03-2017 Martins Gomes, R., Baunach, M., Batista Ribeiro, L.: MCSmartOS: A Dependable OS for Compositional Embedded Systems. (2017). FoE-Tag des Field of Expertise “Information, Communication and Computing” ; Conference date: 28-03-2017
24.
Zurück zum Zitat Batista Ribeiro, L., Lorber, F., Nyman, U., Larsen, K.G., Baunach, M.: A modeling concept for formal verification of os-based compositional software. In: Currently Under Review. UnderReview’22. Association for Computing Machinery, New York, NY, USA (2022) Batista Ribeiro, L., Lorber, F., Nyman, U., Larsen, K.G., Baunach, M.: A modeling concept for formal verification of os-based compositional software. In: Currently Under Review. UnderReview’22. Association for Computing Machinery, New York, NY, USA (2022)
25.
Zurück zum Zitat Barbot, B., Basset, N., Beunardeau, M., Kwiatkowska, M.: Uniform sampling for timed automata with application to language inclusion measurement. In: Agha, G., Van Houdt, B. (eds.) Quantitative Evaluation of Systems, pp. 175–190. Springer, Cham (2016)CrossRef Barbot, B., Basset, N., Beunardeau, M., Kwiatkowska, M.: Uniform sampling for timed automata with application to language inclusion measurement. In: Agha, G., Van Houdt, B. (eds.) Quantitative Evaluation of Systems, pp. 175–190. Springer, Cham (2016)CrossRef
Metadaten
Titel
Randomized reachability analysis in UPPAAL: fast error detection in timed systems
verfasst von
Andrej Kiviriga
Kim Guldstrand Larsen
Ulrik Nyman
Publikationsdatum
17.11.2022
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 6/2022
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00681-z

Weitere Artikel der Ausgabe 6/2022

International Journal on Software Tools for Technology Transfer 6/2022 Zur Ausgabe

Premium Partner