{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T04:11:08Z","timestamp":1750911068074,"version":"3.41.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319682693"},{"type":"electronic","value":"9783319682709"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68270-9_6","type":"book-chapter","created":{"date-parts":[[2017,9,26]],"date-time":"2017-09-26T11:17:19Z","timestamp":1506424639000},"page":"107-124","source":"Crossref","is-referenced-by-count":2,"title":["Compositional Testing of Real-Time Systems"],"prefix":"10.1007","author":[{"given":"Kim G.","family":"Larsen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Miku\u010dionis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brian","family":"Nielsen","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":[[2017,9,27]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1016\/j.tcs.2011.12.072","volume":"455","author":"M Aiguier","year":"2012","unstructured":"Aiguier, M., Boulanger, F., Kanso, B.: A formal abstract framework for modelling and testing complex software systems. Theoret. Comput. Sci. 455, 66\u201397 (2012). International Colloquium on Theoretical Aspects of Computing (2010)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"6_CR2","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. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR3","unstructured":"Kanso, B., Chebaro, O.: Compositional testing for FSM-based models. Int. J. Softw. Eng. Appl. (IJSEA) 5(3) (2014)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Boudjadar, A., David, A., Kim, J.H., Larsen, K.G., Mikucionis, M., Nyman, U., Skou, A.: Degree of schedulability of mixed-criticality real-time systems with probabilistic sporadic tasks. In: 2014 Theoretical Aspects of Software Engineering Conference, TASE 2014, Changsha, China, 1\u20133 September 2014, pp. 126\u2013130. IEEE Computer Society (2014)","DOI":"10.1109\/TASE.2014.27"},{"key":"6_CR5","unstructured":"Briones, L.B.: Assume-guarantee reasoning with ioco testing relation. In: Proceedings of the 22nd IFIP International Conference on Testing Software and Systems (2010)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-35632-2_25","volume-title":"Runtime Verification","author":"P Bulychev","year":"2013","unstructured":"Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of WMTL. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 260\u2013275. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35632-2_25"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-28717-6_15","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P Bulychev","year":"2012","unstructured":"Bulychev, P., David, A., Guldstrand Larsen, K., Legay, A., Li, G., B\u00f8gsted Poulsen, D., Stainer, A.: Monitor-based statistical model checking for weighted metric temporal logic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 168\u2013182. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28717-6_15"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-642-28891-3_39","volume-title":"NASA Formal Methods","author":"P Bulychev","year":"2012","unstructured":"Bulychev, P., David, A., Guldstrand Larsen, K., Legay, A., Miku\u010dionis, M., B\u00f8gsted Poulsen, D.: Checking and distributing statistical model checking. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 449\u2013463. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28891-3_39"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Daca, P., Henzinger, T.A., Krenn, W., Nickovic, D.: Compositional specifications for ioco testing. In: Seventh IEEE International Conference on Software Testing, Verification and Validation, ICST, 31 March 2014\u20134 April 2014, Cleveland, Ohio, USA, pp. 373\u2013382. IEEE Computer Society (2014)","DOI":"10.1109\/ICST.2014.50"},{"issue":"12","key":"6_CR10","doi-asserted-by":"crossref","first-page":"2694","DOI":"10.1007\/s11432-012-4742-0","volume":"55","author":"A David","year":"2012","unstructured":"David, A., Du, D., Larsen, K.G., Mikucionis, M., Skou, A.: An evaluation framework for energy aware buildings using statistical model checking. Sci. China Inf. Sci. 55(12), 2694\u20132707 (2012)","journal-title":"Sci. China Inf. Sci."},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-642-34032-1_28","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies","author":"A David","year":"2012","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M.: Schedulability of herschel-planck revisited using statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7610, pp. 293\u2013307. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-34032-1_28"},{"issue":"4","key":"6_CR12","doi-asserted-by":"crossref","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. STTT 17(4), 397\u2013415 (2015)","journal-title":"STTT"},{"issue":"3","key":"6_CR13","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/s10009-014-0323-4","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for biological systems. STTT 17(3), 351\u2013367 (2015)","journal-title":"STTT"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-24310-3_7","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80\u201396. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24310-3_7"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-642-22110-1_27","volume-title":"Computer Aided Verification","author":"A David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349\u2013355. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_27"},{"issue":"1","key":"6_CR16","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/s10009-013-0286-x","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., Traonouez, L., Wasowski, A.: Real-time specifications. STTT 17(1), 17\u201345 (2015)","journal-title":"STTT"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-15643-4_29","volume-title":"Automated Technology for Verification and Analysis","author":"A David","year":"2010","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., W\u0105sowski, A.: ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 365\u2013370. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15643-4_29"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I\/O automata: a complete specification theory for real-time systems. In: Johansson and Yi [21], pp. 91\u2013100","DOI":"10.1145\/1755952.1755967"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"David, N., David, A., Hansen, R.R., Larsen, K.G., Legay, A., Olesen, M.C., Probst, C.W.: Modelling social-technical attacks with timed automata. In: Bertino, E., You, I. (eds.) Proceedings of the 7th ACM CCS International Workshop on Managing Insider Security Threats, MIST 2015, Denver, Colorado, USA, 16 October 2015, pp. 21\u201328. ACM (2015)","DOI":"10.1145\/2808783.2808787"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-78917-8_3","volume-title":"Formal Methods and Testing","author":"A Hessel","year":"2008","unstructured":"Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 77\u2013117. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78917-8_3"},{"key":"6_CR21","unstructured":"Johansson, K.H., Yi, W. (eds.): Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, 12\u201315 April 2010. ACM (2010)"},{"issue":"3","key":"6_CR22","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/s10703-009-0065-1","volume":"34","author":"M Krichen","year":"2009","unstructured":"Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Form. Methods Syst. Des. 34(3), 238\u2013304 (2009)","journal-title":"Form. Methods Syst. Des."},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Mikucionis, M., Nielsen, B., Skou, A.: Testing real-time embedded software using uppaal-tron: an industrial case study. In: Proceedings of the 5th ACM International Conference on Embedded Software, EMSOFT 2005, pp. 299\u2013306. ACM, New York (2005)","DOI":"10.1145\/1086228.1086283"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-540-31848-4_6","volume-title":"Formal Approaches to Software Testing","author":"KG Larsen","year":"2005","unstructured":"Larsen, K.G., Mikucionis, M., Nielsen, B.: Online testing of real-time systems using Uppaal. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 79\u201394. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-31848-4_6"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Miku\u010dionis, M., Larsen, K.G., Nielsen, B.: T-uppaal: online model-based testing of real-time systems. In: Proceedings of the 19th IEEE International Conference on Automated Software Engineering, ASE 2004, pp. 396\u2013397. IEEE Computer Society, Washington, DC, USA (2004)","DOI":"10.1109\/ASE.2004.1342774"},{"key":"6_CR26","unstructured":"Tretmans, J.: A formal approach to conformance testing. In: Rafiq, O. (ed.) Protocol Test Systems, VI, Proceedings of the IFIP TC6\/WG6.1 Sixth International Workshop on Protocol Test Systems, Pau, France, 28\u201330 September 1993. IFIP Transactions, vol. C-19, pp. 257\u2013276. North-Holland (1993)"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-24617-6_7","volume-title":"Formal Approaches to Software Testing","author":"M Bijl van der","year":"2004","unstructured":"van der Bijl, M., Rensink, A., Tretmans, J.: Compositional testing with ioco. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 86\u2013100. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24617-6_7"},{"issue":"4","key":"6_CR28","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/s00446-015-0262-7","volume":"29","author":"RJ Glabbeek van","year":"2016","unstructured":"van Glabbeek, R.J., H\u00f6fner, P., Portmann, M., Tan, W.L.: Modelling and verifying the AODV routing protocol. Distrib. Comput. 29(4), 279\u2013315 (2016)","journal-title":"Distrib. Comput."}],"container-title":["Lecture Notes in Computer Science","ModelEd, TestEd, TrustEd"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68270-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T22:11:06Z","timestamp":1750889466000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68270-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319682693","9783319682709"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68270-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}