{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T15:49:34Z","timestamp":1773330574061,"version":"3.50.1"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2022,11,17]],"date-time":"2022-11-17T00:00:00Z","timestamp":1668643200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,11,17]],"date-time":"2022-11-17T00:00:00Z","timestamp":1668643200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.1007\/s10009-022-00681-z","type":"journal-article","created":{"date-parts":[[2022,11,17]],"date-time":"2022-11-17T14:07:46Z","timestamp":1668694066000},"page":"1025-1042","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Randomized reachability analysis in UPPAAL: fast error detection in timed systems"],"prefix":"10.1007","volume":"24","author":[{"given":"Andrej","family":"Kiviriga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ulrik","family":"Nyman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,11,17]]},"reference":[{"key":"681_CR1","doi-asserted-by":"crossref","unstructured":"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\u201388. Springer, Cham (2020)","DOI":"10.1007\/978-3-030-62822-2_5"},{"key":"681_CR2","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-31980-1_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Grosu","year":"2005","unstructured":"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\u2013286. Springer, Berlin, Heidelberg (2005)"},{"key":"681_CR3","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Formal Methods for the Design of Real-time Systems, pp. 200\u2013236. Springer (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"issue":"5","key":"681_CR4","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1093\/comjnl\/29.5.390","volume":"29","author":"M Joseph","year":"1986","unstructured":"Joseph, M., Pandya, P.: Finding response times in a real-time system. Comput. J. 29(5), 390\u2013395 (1986). https:\/\/doi.org\/10.1093\/comjnl\/29.5.390","journal-title":"Comput. J."},{"key":"681_CR5","unstructured":"Burns, A.: Preemptive Priority-Based Scheduling: An Appropriate Engineering Approach, pp. 225\u2013248. Prentice-Hall, Inc., Hoboken (1995)"},{"key":"681_CR6","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.scico.2016.05.008","volume":"127","author":"A Boudjadar","year":"2016","unstructured":"Boudjadar, A., David, A., Kim, J., Larsen, K., Miku\u010dionis, M., Nyman, U., Skou, A.: Statistical and exact schedulability analysis of hierarchical scheduling systems. Sci. Comput. Program. 127, 103\u2013130 (2016). https:\/\/doi.org\/10.1016\/j.scico.2016.05.008","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"681_CR7","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1016\/j.scico.2015.10.003","volume":"113","author":"A Boudjadar","year":"2015","unstructured":"Boudjadar, A., David, A., Kim, J., Larsen, K., Miku\u010dionis, M., Nyman, U., Skou, A.: A reconfigurable framework for compositional schedulability and power analysis of hierarchical scheduling systems with frequency scaling. Sci. Comput. Program. 113(3), 236\u2013260 (2015). https:\/\/doi.org\/10.1016\/j.scico.2015.10.003","journal-title":"Sci. Comput. Program."},{"key":"681_CR8","doi-asserted-by":"publisher","unstructured":"Brekling, A., Hansen, M.R., Madsen, J.: Moves - a framework for modelling and verifying embedded systems. In: 2009 International Conference on Microelectronics - ICM, pp. 149\u2013152 (2009). https:\/\/doi.org\/10.1109\/ICM.2009.5418667","DOI":"10.1109\/ICM.2009.5418667"},{"key":"681_CR9","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-642-16561-0_21","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"M Miku\u010dionis","year":"2010","unstructured":"Miku\u010dionis, M., Larsen, K.G., Rasmussen, J.I., Nielsen, B., Skou, A., Palm, S.U., Pedersen, J.S., Hougaard, P.: Schedulability analysis using uppaal: Herschel\u2013Planck case study. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification, and Validation, pp. 175\u2013190. Springer, Berlin, Heidelberg (2010)"},{"issue":"1","key":"681_CR10","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1201\/9781420067859-c4","volume":"1","author":"A David","year":"2009","unstructured":"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\u2013119 (2009)","journal-title":"Model-Based Design Embedded Syst."},{"key":"681_CR11","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M.: Schedulability of Herschel\u2013Planck 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\u2013307. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-34032-1_28"},{"key":"681_CR12","volume-title":"Herschel-planck acc asw: sizing, timing and schedulability analysis","author":"S Palm","year":"2006","unstructured":"Palm, S.: Herschel-planck acc asw: sizing, timing and schedulability analysis. Tech. rep., Terma A\/S, Technical report (2006)"},{"key":"681_CR13","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/3-540-44618-4_12","volume-title":"CONCUR 2000\u2013Concurrency Theory","author":"F Cassez","year":"2000","unstructured":"Cassez, F., Larsen, K.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000\u2013Concurrency Theory, pp. 138\u2013152. Springer, Berlin, Heidelberg (2000)"},{"issue":"8","key":"681_CR14","doi-asserted-by":"publisher","first-page":"1149","DOI":"10.1016\/j.ic.2007.01.009","volume":"205","author":"E Fersman","year":"2007","unstructured":"Fersman, E., Krcal, P., Pettersson, P., Yi, W.: Task automata: Schedulability, decidability and undecidability. Inform. Comput. 205(8), 1149\u20131172 (2007). https:\/\/doi.org\/10.1016\/j.ic.2007.01.009","journal-title":"Inform. Comput."},{"key":"681_CR15","doi-asserted-by":"crossref","unstructured":"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\u2013215. Springer, Berlin, Heidelberg (2004)","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"681_CR16","unstructured":"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\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) Runtime Verification, pp. 122\u2013135. Springer, Berlin, Heidelberg (2010)"},{"issue":"4","key":"681_CR17","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Software Tools Technol. Transf. 17(4), 397\u2013415 (2015)","journal-title":"Int. J. Software Tools Technol. Transf."},{"key":"681_CR18","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BFb0031987","volume-title":"Real-Time: Theory in Practice","author":"R Alur","year":"1992","unstructured":"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\u201373. Springer, Berlin, Heidelberg (1992)"},{"key":"681_CR19","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/11561163_8","volume-title":"Formal Methods Comp. Obj.","author":"G Behrmann","year":"2005","unstructured":"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\u2013182. Springer, Berlin, Heidelberg (2005)"},{"key":"681_CR20","doi-asserted-by":"crossref","unstructured":"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\u2013169. Springer, Cham (2017)","DOI":"10.1007\/978-3-319-72308-2_10"},{"key":"681_CR21","doi-asserted-by":"publisher","unstructured":"Han, P., Zhai, Z., Nielsen, B., Nyman, U.: Model-based optimization of arinc-653 partition scheduling. Int. J. Software Tools Technol. Transf. (2021). https:\/\/doi.org\/10.1007\/s10009-020-00597-6","DOI":"10.1007\/s10009-020-00597-6"},{"key":"681_CR22","unstructured":"S\u00f8e\u00a0Luckow, K., B\u00f8gholm, T., Thomsen, B.: A Flexible Schedulability Analysis Tool for SCJ Programs. http:\/\/people.cs.aau.dk\/~boegholm\/tetasarts\/. Accessed: 2021-05-07"},{"key":"681_CR23","unstructured":"Martins Gomes, R., Baunach, M., Batista Ribeiro, L.: MCSmartOS: A Dependable OS for Compositional Embedded Systems. (2017). FoE-Tag des Field of Expertise \u201cInformation, Communication and Computing\u201d ; Conference date: 28-03-2017"},{"key":"681_CR24","doi-asserted-by":"crossref","unstructured":"Batista\u00a0Ribeiro, 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\u201922. Association for Computing Machinery, New York, NY, USA (2022)","DOI":"10.1007\/978-3-031-30826-0_2"},{"key":"681_CR25","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-319-43425-4_13","volume-title":"Quantitative Evaluation of Systems","author":"B Barbot","year":"2016","unstructured":"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\u2013190. Springer, Cham (2016)"},{"key":"681_CR26","unstructured":"Onis, R.: UrPal. https:\/\/github.com\/utwente-fmt\/UrPal. Accessed 18 May2021"},{"key":"681_CR27","unstructured":"Onis, R.: Does your model make sense? Automatic verification of timed systems (2018). http:\/\/essay.utwente.nl\/77031\/"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00681-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00681-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00681-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,1]],"date-time":"2023-12-01T09:32:30Z","timestamp":1701423150000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00681-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,17]]},"references-count":27,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["681"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00681-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,11,17]]},"assertion":[{"value":"18 October 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 November 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}