{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:43:56Z","timestamp":1779392636576,"version":"3.53.1"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,1,6]],"date-time":"2015-01-06T00:00:00Z","timestamp":1420502400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,8]]},"DOI":"10.1007\/s10009-014-0361-y","type":"journal-article","created":{"date-parts":[[2015,1,5]],"date-time":"2015-01-05T14:40:52Z","timestamp":1420468852000},"page":"397-415","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":422,"title":["Uppaal SMC tutorial"],"prefix":"10.1007","volume":"17","author":[{"given":"Alexandre","family":"David","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marius","family":"Miku\u010dionis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Danny B\u00f8gsted","family":"Poulsen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,1,6]]},"reference":[{"issue":"2","key":"361_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"361_CR2","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996)","journal-title":"J. ACM"},{"key":"361_CR3","doi-asserted-by":"crossref","unstructured":"Boyer, B., Corre, K., Legay, A., Sedwards, S.: Plasma-lab: a flexible, distributable statistical model checking library. In: QEST, pp. 160\u2013164 (2013)","DOI":"10.1007\/978-3-642-40196-1_12"},{"key":"361_CR4","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. Lecture Notes in Computer Science. pp. 200\u2013236 (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"issue":"2","key":"361_CR5","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1002\/spe.1006","volume":"41","author":"G Behrmann","year":"2011","unstructured":"Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing uppaal over 15 years. Softw. Pract. Exp. 41(2), 133\u2013142 (2011)","journal-title":"Softw. Pract. Exp."},{"key":"361_CR6","doi-asserted-by":"crossref","unstructured":"Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of wmtl. In: Runtime Verification, vol. 7687 of LNCS, pp. 260\u2013275 (2012)","DOI":"10.1007\/978-3-642-35632-2_25"},{"key":"361_CR7","doi-asserted-by":"crossref","unstructured":"Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B., Stainer, A.: Monitor-based statistical model checking for weighted metric temporal logic. In: Nikolaj, B., Voronkov, A. (eds.) 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, vol. 7180 of LNCS, pp. 168\u2013182. Springer (2012)","DOI":"10.1007\/978-3-642-28717-6_15"},{"key":"361_CR8","doi-asserted-by":"crossref","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Checking and distributing statistical model checking. In: NASA Formal Methods, vol. 7226 of Lecture Notes in Computer Science, pp. 449\u2013463. Springer (2012)","DOI":"10.1007\/978-3-642-28891-3_39"},{"key":"361_CR9","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., Yi, W.: Unification & sharing in timed automata verification. In: SPIN Workshop 03, vol. 2648 of LNCS, pp. 225\u2013229 (2003)","DOI":"10.1007\/3-540-44829-2_15"},{"issue":"1","key":"361_CR10","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/s10009-003-0111-z","volume":"7","author":"G Behrmann","year":"2005","unstructured":"Behrmann, G.: Distributed reachability analysis in timed automata. STTT 7(1), 19\u201330 (2005)","journal-title":"STTT"},{"key":"361_CR11","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.: Efficient guiding towards cost-optimality in uppaal. In: Margaria, T., Yi, W. (eds.) Proceedings of the 7th International Conference on Tools and Algorithms for the construction and analysis of systems, number 2031 in Lecture Notes in Computer Science, pp. 174\u2013188. Springer (2001)","DOI":"10.1007\/3-540-45319-9_13"},{"key":"361_CR12","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) Proceedings of the 4th International Workshop on Hybris Systems: Computation and Control, number 2034 in Lecture Notes in Computer Sciences, pp. 147\u2013161 Springer-Verlag (2001)","DOI":"10.7146\/brics.v8i3.20457"},{"key":"361_CR13","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Hune, T., Vaandrager, F.: Distributed timed model checking: How the search order matters. In: Proceedings of 12th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Chicago, Springer, Jul (2000)","DOI":"10.1007\/10722167_19"},{"key":"361_CR14","doi-asserted-by":"crossref","unstructured":"Broy, M., Jonsson, B., Katoen, J-P., Leucker, M., Pretschner, A. (eds.): Model-based testing of reactive systems, advanced lectures the volume is the outcome of a research seminar that was held in Schloss Dagstuhl in January 2004, vol. 3472 of Lecture Notes in Computer Science. Springer (2005)","DOI":"10.1007\/b137241"},{"key":"361_CR15","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference d iagrams. In: Proceedings of the 12th Int. Conf. on Computer Aided Verificat ion, vol. 1633 of Lecture Notes in Computer Science. Springer (1999)","DOI":"10.1007\/3-540-48683-6_30"},{"key":"361_CR16","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Faeder, J.R., Langmead, C.J., Harris, L.A., Jha, S.K., Legay, A.: Statistical model checking in biolab: applications to the automated analysis of t-cell receptor signaling pathway. In: CMSB, LNCS, pp. 231\u2013250 (2008)","DOI":"10.1007\/978-3-540-88562-7_18"},{"key":"361_CR17","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"4","key":"361_CR18","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1214\/aoms\/1177729330","volume":"23","author":"H Chernoff","year":"1952","unstructured":"Chernoff, H.: A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations. Ann. Math. Stat. 23(4), 493\u2013507 (1952)","journal-title":"Ann. Math. Stat."},{"issue":"4","key":"361_CR19","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1093\/biomet\/26.4.404","volume":"26","author":"CJ Clopper","year":"1934","unstructured":"Clopper, C.J., Pearson, E.S.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26(4), 404\u2013413 (1934)","journal-title":"Biometrika"},{"key":"361_CR20","doi-asserted-by":"crossref","unstructured":"David, A., Du, D., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for stochastic hybrid systems. In: Bartocci, E., Bortolussi, L. (eds.) HSB, vol. 92 of EPTCS, pp. 122\u2013136 (2012)","DOI":"10.4204\/EPTCS.92.9"},{"key":"361_CR21","doi-asserted-by":"crossref","unstructured":"David, A., Du, D., Larsen, K.G., Legay, A., Miku\u010dionis, M.: Optimizing control strategy using statistical model checking. In: NASA formal methods, vol. 7871 of Lecture Notes in Computer Science, pp. 352\u2013367. Springer (2013)","DOI":"10.1007\/978-3-642-38088-4_24"},{"key":"361_CR22","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., S\u00f8resensen, M.G., Taankvist, J.H.: On time with miniam expected cost"},{"key":"361_CR23","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., Vliet, J.V., Wang, Z.: Statistical model checking for networks of priced timed automata. In: FORMATS, LNCS, pp. 80\u201396. Springer (2011)","DOI":"10.1007\/978-3-642-24310-3_7"},{"key":"361_CR24","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., Sedwards, S.: Runtime verification of biological systems. In: Margaria, T., Steffen, B. (eds.), ISoLA (1), vol. 7609 of Lecture Notes in Computer Science, pp. 388\u2013404. Springer (2012)","DOI":"10.1007\/978-3-642-34026-0_29"},{"key":"361_CR25","doi-asserted-by":"crossref","unstructured":"David, A., M\u00f6ller, M.O., Yi, W.: Formal verification of UML statecharts with real-time extensions. In: Kutsche, R.-D., Weber, H. (eds.) Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, vol. 2306 of LNCS, pp. 218\u2013232. Springer (2002)","DOI":"10.1007\/3-540-45923-5_15"},{"key":"361_CR26","doi-asserted-by":"crossref","unstructured":"Henriques, D., Martins, J.G., Zuliani, P., Platzer, A., Clarke, E.M.: Statistical model checking for markov decision processes. In: Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012, London, United Kingdom, Sept 17\u201320, 2012, pp. 84\u201393. IEEE Computer Society (2012)","DOI":"10.1109\/QEST.2012.19"},{"key":"361_CR27","doi-asserted-by":"crossref","unstructured":"Hartmanns, A.: Model-checking and simulation for stochastic timed systems. In: Bernhard, K.A., De Boer, F.S., Marcello M.B. (eds.) FMCO, vol. 6957 of Lecture Notes in Computer Science, pp. 372\u2013391. Springer (2010)","DOI":"10.1007\/978-3-642-25271-6_20"},{"key":"361_CR28","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Ho, P.-H.: Algorithmic analysis of nonlinear hybrid systems. In: Wolper, P. (ed.) Computer Aided Verification, 7th International Conference, Li\u00e8ge, Belgium, July, 3\u20135, 1995, Proceedings, vol. 939 of Lecture Notes in Computer Science, pp. 225\u2013238. Springer (1995)","DOI":"10.1007\/3-540-60045-0_53"},{"key":"361_CR29","doi-asserted-by":"crossref","unstructured":"Hendriks, M., Larsen, K.G.: Exact acceleration of real-time model checking. In: Asarin, E., Maler, O., Yovine, S. (eds.) Electronic Notes in Theoretical Computer Science, vol. 65. Elsevier Science Publishers (2002)","DOI":"10.1016\/S1571-0661(04)80473-0"},{"key":"361_CR30","doi-asserted-by":"crossref","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) Verification, Model Checking, and Abstract Interpretation, vol. 2937 of Lecture Notes in Computer Science, pp. 73\u201384. Springer, Berlin, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24622-0_8"},{"issue":"301","key":"361_CR31","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","volume":"58","author":"W Hoeffding","year":"1963","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13\u201330 (1963)","journal-title":"J. Am. Stat. Assoc."},{"key":"361_CR32","doi-asserted-by":"crossref","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: CMSB, vol. 5688 of LNCS, pp. 218\u2013234. Springer (2009)","DOI":"10.1007\/978-3-642-03845-7_15"},{"key":"361_CR33","doi-asserted-by":"crossref","unstructured":"J\u00e9gourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: CAV, vol. 8044 of Lecture Notes in Computer Science, pp. 576\u2013591. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_38"},{"key":"361_CR34","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism 2.0: A tool for probabilistic model checking. In: Proc. of 1th Int. Conference on the Quantitative Evaluation of Systems (QEST), pp. 322\u2013323. IEEE (2004)","DOI":"10.1109\/QEST.2004.1348048"},{"key":"361_CR35","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.: As cheap as possible: efficient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) Proceedings of CAV 2001, number 2102 in Lecture Notes in Computer Science, pp. 493\u2013505. Springer (2001)","DOI":"10.1007\/3-540-44585-4_47"},{"key":"361_CR36","doi-asserted-by":"crossref","unstructured":"Larsson, F., Larsen, K.G.,Pettersson, P., Yi, W.: Efficient verification of real-time systems: Compact data structures and state-space reduction. In: Proc. of the 18th IEEE Real-Time Systems Symposium, pp. 14\u201324. IEEE Computer Society Press (1997)","DOI":"10.1109\/REAL.1997.641265"},{"key":"361_CR37","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997)","DOI":"10.1007\/s100090050010"},{"key":"361_CR38","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: CAV, LNCS 3114, pp. 202\u2013215. Springer (2004)","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"361_CR39","unstructured":"Theelen, B.D.: Performance modelling for system-level design. Ph.D. thesis, Eindhoven University of Technology, (2004) ISBN 90-386-1633-3"},{"issue":"2","key":"361_CR40","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945)","journal-title":"Ann. Math. Stat."},{"key":"361_CR41","unstructured":"Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon (2005)"},{"key":"361_CR42","doi-asserted-by":"crossref","unstructured":"Yi, W., Pettersson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, pp. 243\u2013258, London, UK, UK, Chapman & Hall Ltd (1995)","DOI":"10.1007\/978-0-387-34878-0_18"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0361-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0361-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0361-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,25]],"date-time":"2022-04-25T23:55:10Z","timestamp":1650930910000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0361-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,6]]},"references-count":42,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["361"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0361-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,1,6]]}}}