{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T00:18:11Z","timestamp":1743034691089,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319307336"},{"type":"electronic","value":"9783319307343"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-30734-3_4","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T08:19:52Z","timestamp":1457770792000},"page":"15-32","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Conformance Checking of Real-Time Models"],"prefix":"10.1007","author":[{"given":"Bernhard K.","family":"Aichernig","sequence":"first","affiliation":[]},{"given":"Florian","family":"Lorber","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Tappler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,3,13]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"612","DOI":"10.1007\/978-3-642-05089-3_39","volume-title":"FM 2009: Formal Methods","author":"W Ahrendt","year":"2009","unstructured":"Ahrendt, W., de Boer, F.S., Grabe, I.: Abstract object creation in dynamic logic. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 612\u2013627. Springer, Heidelberg (2009)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-17071-3_12","volume-title":"Formal Methods for Components and Objects","author":"BK Aichernig","year":"2010","unstructured":"Aichernig, B.K., Brandl, H., J\u00f6bstl, E., Krenn, W.: Model-based mutation testing of hybrid systems. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 228\u2013249. Springer, Heidelberg (2010)"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"716","DOI":"10.1002\/stvr.1522","volume":"25","author":"BK Aichernig","year":"2014","unstructured":"Aichernig, B.K., Brandl, H., J\u00f6bstl, E., Krenn, W., Schlick, R., Tiran, S.: Killing strategies for model-based mutation testing. Softw. Test. Verification Reliab. 25, 716\u2013748 (2014)","journal-title":"Softw. Test. Verification Reliab."},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1016\/j.scico.2014.05.004","volume":"97","author":"BK Aichernig","year":"2015","unstructured":"Aichernig, B.K., J\u00f6bstl, E., Tiran, S.: Model-based mutation testing via symbolic refinement checking. Sci. Comput. Program. 97, 383\u2013404 (2015)","journal-title":"Sci. Comput. Program."},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-38916-0_2","volume-title":"Tests and Proofs","author":"BK Aichernig","year":"2013","unstructured":"Aichernig, B.K., Lorber, F., Ni\u010dkovi\u0107, D.: Time for mutants \u2014 Model-based mutation testing with timed automata. In: Veanes, M., Vigan\u00f2, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 20\u201338. Springer, Heidelberg (2013)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., Tappler, M.: Symbolic input-output conformance checking for model-based mutation testing. In: USE (2015)","DOI":"10.1016\/j.entcs.2016.01.002"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Albert, E., de Boer, F.S., H\u00e4hnle, R., Johnsen, E.B., Laneve, C.: Engineering virtualized services. In: Second Nordic Symposium on Cloud Computing & Internet Technologies, NordiCloud 2013, Oslo, Norway, 1\u20133 September 2013, pp. 59\u201363 (2013)","DOI":"10.1145\/2513534.2513545"},{"issue":"4","key":"4_CR8","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s11761-013-0148-0","volume":"8","author":"E Albert","year":"2014","unstructured":"Albert, E., de Boer, F.S., H\u00e4hnle, R., Johnsen, E.B., Schlatte, R., Tarifa, S.L.T., Wong, Y.H.: Formal modeling and analysis of resource management for cloud architectures: an industrial case study using real-time ABS. Serv. Oriented Comput. Appl. 8(4), 323\u2013339 (2014)","journal-title":"Serv. Oriented Comput. Appl."},{"issue":"2","key":"4_CR9","doi-asserted-by":"publisher","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."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Back, R.-J., Kurki-Suonio, R.: Decentralization of process nets withcentralized control. In: Proceedings of the Second Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, 17-19 August 1983, pp. 131\u2013142 (1983)","DOI":"10.1145\/800221.806716"},{"issue":"2\u20133","key":"4_CR11","doi-asserted-by":"crossref","first-page":"145","DOI":"10.3233\/FI-1998-36233","volume":"36","author":"B B\u00e9rard","year":"1998","unstructured":"B\u00e9rard, B., Petit, A., Diekert, V., Gastin, P.: Characterization of the expressive power of silent transitions in timed automata. Fundam. Inform. 36(2\u20133), 145\u2013182 (1998)","journal-title":"Fundam. Inform."},{"issue":"1","key":"4_CR12","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/s11334-012-0184-5","volume":"9","author":"J Bj\u00f8rk","year":"2013","unstructured":"Bj\u00f8rk, J., de Boer, F.S., Johnsen, E.B., Schlatte, R., Tarifa, S.L.T.: User-defined schedulers for real-time concurrent objects. Innovations Syst. Softw. Eng. (ISSE) 9(1), 29\u201343 (2013)","journal-title":"Innovations Syst. Softw. Eng. (ISSE)"},{"issue":"2","key":"4_CR13","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82\u201390 (2013)","journal-title":"Commun. ACM"},{"issue":"5","key":"4_CR14","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0020-0190(72)90034-8","volume":"1","author":"EW Dijkstra","year":"1972","unstructured":"Dijkstra, E.W.: Information streams sharing a finite buffer. Inf. Process. Lett. 1(5), 179\u2013180 (1972)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"4_CR15","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/BF01211618","volume":"9","author":"CJ Fidge","year":"1997","unstructured":"Fidge, C.J., Wellings, A.J.: An action-based formal model for concurrent real-time systems. Formal Aspects Comput. 9(2), 175\u2013207 (1997)","journal-title":"Formal Aspects Comput."},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/11940197_3","volume-title":"Formal Approaches to Software Testing and Runtime Verification","author":"L Frantzen","year":"2006","unstructured":"Frantzen, L., Tretmans, J., Willemse, T.A.C.: A symbolic framework for model-based testing. In: Havelund, K., N\u00fa\u00f1ez, M., Ro\u015fu, G., Wolff, B. (eds.) FATES 2006 and RV 2006. LNCS, vol. 4262, pp. 40\u201354. Springer, Heidelberg (2006)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11754008_1","volume-title":"Testing of Communicating Systems","author":"C Gaston","year":"2006","unstructured":"Gaston, C., Le Gall, P., Rapin, N., Touil, A.: Symbolic execution techniques for test purpose definition. In: Uyar, M.U., Duale, A.Y., Fecko, M.A. (eds.) TestCom 2006. LNCS, vol. 3964, pp. 1\u201318. Springer, Heidelberg (2006)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Jaghoori, M.M., Longuet, D., de Boer, F.S., Chothia, T.: Schedulability and compatibility of real time asynchronous objects. In: Real-Time Systems Symposium 2008, pp. 70\u201379, November 2008","DOI":"10.1109\/RTSS.2008.28"},{"issue":"3","key":"4_CR19","doi-asserted-by":"publisher","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. Formal Methods Syst. Des. 34(3), 238\u2013304 (2009)","journal-title":"Formal Methods Syst. Des."},{"issue":"2\u20133","key":"4_CR20","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/s00446-003-0090-z","volume":"16","author":"R Kurki-Suonio","year":"2003","unstructured":"Kurki-Suonio, R.: Action systems in incremental and aspect-oriented modeling. Distrib. Comput. 16(2\u20133), 201\u2013217 (2003)","journal-title":"Distrib. Comput."},{"issue":"1\u20132","key":"4_CR21","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1\u20132), 134\u2013152 (1997)","journal-title":"STTT"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-319-22975-1_19","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"F Lorber","year":"2015","unstructured":"Lorber, F., Rosenmann, A., Ni\u010dkovi\u0107, D., Aichernig, B.K.: Bounded determinization of timed automata with silent transitions. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 288\u2013304. Springer, Heidelberg (2015)"},{"issue":"7\u20138","key":"4_CR23","doi-asserted-by":"publisher","first-page":"799","DOI":"10.1016\/j.scico.2011.04.002","volume":"77","author":"S Meng","year":"2012","unstructured":"Meng, S., Arbab, F., Aichernig, B.K., Astefanoaei, L., de Boer, F.S., Rutten, J.J.M.M.: Connectors as designs: Modeling, refinement and test case generation. Sci. Comput. Program. 77(7\u20138), 799\u2013822 (2012)","journal-title":"Sci. Comput. Program."},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-85762-4_22","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"R Schlatte","year":"2008","unstructured":"Schlatte, R., Aichernig, B.K., de Boer, F.S., Griesmayer, A., Johnsen, E.B.: Testing concurrent objects with application-specific schedulers. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 319\u2013333. Springer, Heidelberg (2008)"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78917-8_1","volume-title":"Formal Methods and Testing","author":"J Tretmans","year":"2008","unstructured":"Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 1\u201338. Springer, Heidelberg (2008)"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-15297-9_19","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S von Styp","year":"2010","unstructured":"von Styp, S., Bohnenkamp, H., Schmaltz, J.: A conformance testing relation for symbolic timed automata. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 243\u2013255. Springer, Heidelberg (2010)"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Wabenhorst, A.: A model of real-time distributed systems. In: PROCOMET 1998, pp. 462\u2013481. Chapman and Hall (1998)","DOI":"10.1007\/978-0-387-35358-6_29"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-54862-8_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Wang","year":"2014","unstructured":"Wang, T., Sun, J., Liu, Y., Wang, X., Li, S.: Are timed automata bad for a specification language? Language inclusion checking for timed automata. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 310\u2013325. Springer, Heidelberg (2014)"},{"key":"4_CR29","unstructured":"Westerlund, T., Plosila, J.: Formal timing model for hardware components. In: Norchip Conference, 2004. Proceedings, pp. 293\u2013296, November 2004"},{"issue":"1","key":"4_CR30","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10009-014-0301-x","volume":"17","author":"PYH Wong","year":"2015","unstructured":"Wong, P.Y.H., Bubel, R., de Boer, F.S., G\u00f3mez-Zamalloa, M., de Gouw, S., H\u00e4hnle, R., Meinke, K., Sindhu, M.A.: Testing abstract behavioral specifications. Int. J. Softw. Tools Technol. (STTT) 17(1), 107\u2013119 (2015)","journal-title":"Int. J. Softw. Tools Technol. (STTT)"}],"container-title":["Lecture Notes in Computer Science","Theory and Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30734-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T12:25:11Z","timestamp":1720787111000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-30734-3_4"}},"subtitle":["Symbolic Execution vs. Bounded Model Checking"],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319307336","9783319307343"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30734-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}