{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T11:44:37Z","timestamp":1778327077567,"version":"3.51.4"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,6,22]],"date-time":"2012-06-22T00:00:00Z","timestamp":1340323200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s10009-012-0240-3","type":"journal-article","created":{"date-parts":[[2012,7,8]],"date-time":"2012-07-08T21:34:02Z","timestamp":1341783242000},"page":"383-386","source":"Crossref","is-referenced-by-count":21,"title":["Model-based testing of software and systems: recent advances and challenges"],"prefix":"10.1007","volume":"14","author":[{"given":"Alexandre","family":"Petrenko","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adenilso","family":"Simao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9 Carlos","family":"Maldonado","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,6,22]]},"reference":[{"key":"240_CR1","unstructured":"Andrade, W.L., Machado, P.D.L., Jeron, T., Marchand, H.: Abstracting time and data for conformance Testing of teal-time systems. In: A-MOST 2011, 9\u201317 (2011)"},{"key":"240_CR2","doi-asserted-by":"crossref","unstructured":"Bochmann, G.v., Jourdan, G.-V.: Testing k-safe petri nets. In: TestCom\/FATES 09, LNCS, vol. 5826, pp. 33\u201348, Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-05031-2_3"},{"key":"240_CR3","unstructured":"Clarke, D., J\u00e9ron, T., Rusu, V., Zinovieva, E., Katoen, J.-P., Stevens, P.: STG: A symbolic test generation tool. ETAPS 2002 and TACAS 2002, LNCS, vol. 2280, pp. 151\u2013173. Springer, Heidelberg (2002)"},{"issue":"8","key":"240_CR4","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1109\/TSE.2007.70707","volume":"33","author":"C. Constant","year":"2007","unstructured":"Constant C., J\u00e9ron T., Marchand H., Rusu V.: Integrating formal verification and conformance testing for reactive systems. IEEE Trans. Softw. Eng. 33(8), 558\u2013574 (2007)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"240_CR5","doi-asserted-by":"crossref","unstructured":"El-Fakih, K., Yevtushenko, N., Fouchal, H.: Testing timed finite state machines with guaranteed fault coverage. In: TestCom 2009, LNCS, vol. 5826, pp. 66\u201380. Springer, Eindhoven (2009)","DOI":"10.1007\/978-3-642-05031-2_5"},{"issue":"1","key":"240_CR6","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s11219-007-9021-8","volume":"16","author":"En-Nouaary","year":"2008","unstructured":"En-Nouaary , En-Nouaary : A scalable method for testing real-time systems. Softw. Qual. J. 16(1), 3\u201322 (2008)","journal-title":"Softw. Qual. J."},{"key":"240_CR7","unstructured":"Falcone, Y., Fernandez, J.-C., J\u00e9ron, T., Marchand, H., Mounier, L.: More testable properties, in this volume"},{"key":"240_CR8","doi-asserted-by":"crossref","unstructured":"Frantzen, L., Tretmans, J., Willemse, T.: A Symbolic Framework for Model-Based Testing. FATES 2006 and RV 2006. LNCS, vol. 4262, pp. 40\u201354. Springer, Heidelberg (2006)","DOI":"10.1007\/11940197_3"},{"key":"240_CR9","doi-asserted-by":"crossref","unstructured":"Gaston, C., Le Gall, P., Rapin, N., Touil, A.: Symbolic execution techniques for Test Purpose Definition. In: TESTCOM 2006, LNCS, vol. 3964, pp. 1\u201318. Springer, Heidelberg (2006)","DOI":"10.1007\/11754008_1"},{"key":"240_CR10","unstructured":"Gladisch, C.: Model Generation for Quantified Formulas with Application to Test Data Generation, in this volume"},{"issue":"1","key":"240_CR11","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1002\/stvr.427","volume":"21","author":"W. Grieskamp","year":"2011","unstructured":"Grieskamp W., Kicillof N., Stobie K., Braberman V.: Model-based quality assurance of protocol documentation: tools and methodology. Softw. Test. Verification Reliab. 21(1), 55\u201371 (2011)","journal-title":"Softw. Test. Verification Reliab."},{"key":"240_CR12","doi-asserted-by":"crossref","unstructured":"Haar, S., Jard, C., Jourdan, G.-V.: Testing input\/output partial order automata. In: TestCom 2007, LNCS 4581, pp. 171\u2013185, Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73066-8_12"},{"issue":"2","key":"240_CR13","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1016\/j.jss.2009.09.014","volume":"83","author":"J. Hassine","year":"2010","unstructured":"Hassine J., Rilling J., Dssouli R.: An evaluation of timed scenario notations. J. Syst. Softw. 83(2), 326\u2013350 (2010)","journal-title":"J. Syst. Softw."},{"key":"240_CR14","doi-asserted-by":"crossref","unstructured":"Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing Real-Time Systems Using UPPAAL. In: FORTEST 2008. LNCS, vol. 4949, pp. 77\u2013117. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78917-8_3"},{"key":"240_CR15","unstructured":"Hessel, A., Larsen, K.G., Nielsen, B., Pettersson, P., Skou., A.: Time-optimal real-time test case generation using UPPAAL. In: FATES\u201903, LNCS, vol. 2931, pp. 136\u2013151. Springer, Heidelberg (2003)"},{"issue":"12","key":"240_CR16","doi-asserted-by":"crossref","first-page":"1818","DOI":"10.1109\/TC.2010.238","volume":"60","author":"R.M. Hierons","year":"2011","unstructured":"Hierons R.M.: Controllable testing from Nondeterministic Finite State Machines with Multiple Ports. IEEE Trans. Comput. 60(12), 1818\u20131822 (2011)","journal-title":"IEEE Trans. Comput."},{"issue":"1","key":"240_CR17","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1002\/stvr.396","volume":"19","author":"J. Huo","year":"2009","unstructured":"Huo J., Petrenko A.: Transition covering tests for systems with queues. Softw. Test. Verification Reliability 19(1), 55\u201383 (2009)","journal-title":"Softw. Test. Verification Reliability"},{"issue":"12","key":"240_CR18","doi-asserted-by":"crossref","first-page":"805","DOI":"10.1016\/S0950-5849(03)00061-2","volume":"45","author":"C. Jard","year":"2003","unstructured":"Jard C.: Synthesis of distributed testers from true-concurrency models of reactive systems. Int. J. Inform. Softw. Technol. 45(12), 805\u2013814 (2003)","journal-title":"Int. J. Inform. Softw. Technol."},{"issue":"4","key":"240_CR19","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/s10009-004-0153-x","volume":"7","author":"C. Jard","year":"2005","unstructured":"Jard C., J\u00e9ron T.: TGV: theory, principles and algorithms. Softw. Tools Technol. Transf. 7(4), 297\u2013315 (2005)","journal-title":"Softw. Tools Technol. Transf."},{"key":"240_CR20","doi-asserted-by":"crossref","unstructured":"Larsen, K., Mikucionis, M., Nielsen, B., Skou, A.: Testing Teal-time embedded software using UPPAAL-TRON: an industrial case study. In: 5th ACM international conference on Embedded software, pp. 299\u2013306. ACM Press, NY (2005)","DOI":"10.1145\/1086228.1086283"},{"key":"240_CR21","doi-asserted-by":"crossref","unstructured":"Lund, M.S., Refsdal, A., St\u00f8len, K.: Semantics of UML Models for Dynamic Behavior: A survey of different approaches. In: Model-Based Engineering of Embedded Real-Time Systems, LNCS, vol. 6100, pp. 77\u2013103. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-16277-0_4"},{"key":"240_CR22","doi-asserted-by":"crossref","unstructured":"Moore, E.F.: Gedanken-experiments on sequential machines. Automata Studies. vol. 34, 129\u2013153. Princeton University Press, Princeton (1956)","DOI":"10.1515\/9781400882618-006"},{"issue":"1","key":"240_CR23","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1109\/TSE.2004.1265734","volume":"30","author":"A. Petrenko","year":"2004","unstructured":"Petrenko A., Boroday S., Groz R.: Confirming configurations in EFSM testing. IEEE Trans. Softw. Eng. 30(1), 29\u201342 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"240_CR24","unstructured":"Pozo, A., \u00c1rias, J.C.G., Cabral, R.V., Vergilio, S.R. and Nobre, T.: Multi-objective optimization algorithms applied to the class integration and test order problem, in this volume"},{"issue":"2","key":"240_CR25","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1049\/iet-sen.2008.0018","volume":"3","author":"A. Simao","year":"2009","unstructured":"Simao A., Petrenko A., Maldonado J.C.: Comparing finite state machine test coverage criteria. IET Softw. 3(2), 91\u2013105 (2009)","journal-title":"IET Softw."},{"issue":"11","key":"240_CR26","doi-asserted-by":"crossref","first-page":"1252","DOI":"10.1016\/j.infsof.2011.06.006","volume":"53","author":"A. Simao","year":"2011","unstructured":"Simao A., Petrenko A.: Generating asynchronous test cases from test purposes. Inform. Softw. Technol. 53(11), 1252\u20131262 (2011)","journal-title":"Inform. Softw. Technol."},{"issue":"3","key":"240_CR27","first-page":"103","volume":"17","author":"J. Tretmans","year":"1996","unstructured":"Tretmans J.: Test generation with inputs, outputs and repetitive quiescence. Softw. Concept Tools. 17(3), 103\u2013120 (1996)","journal-title":"Softw. Concept Tools."},{"key":"240_CR28","unstructured":"Tretmans, J., Brinksma, E.: TorX: Automated model-based testing. In: First European Conference on Model-Driven Software Engineering, pp. 31\u201343 (2003)"},{"key":"240_CR29","doi-asserted-by":"crossref","unstructured":"Tretmans, J.: Model based testing with labelled transition systems. In: Formal Methods and Testing, LNCS, vol. 4949, pp. 1\u201338. Springer, Berlin, (2008)","DOI":"10.1007\/978-3-540-78917-8_1"},{"key":"240_CR30","unstructured":"Utting, M., Legeard, B.: Practical model-based testing: a tools approach. Morgan Kaufmann, San Francisco (2007)"},{"key":"240_CR31","doi-asserted-by":"crossref","unstructured":"Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., Nachmanson L.: Model-based testing of object-oriented reactive systems with Spec Explore. In: Formal Methods and Testing, LNCS, vol. 4949, pp. 39\u201376. Springer, Berlin, (2008)","DOI":"10.1007\/978-3-540-78917-8_2"},{"key":"240_CR32","unstructured":"Veanes, M., Bj\u00f8rner, N.: Alternating Simulation and IOCO, in this volume."}],"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-012-0240-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0240-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0240-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,30]],"date-time":"2019-06-30T14:21:03Z","timestamp":1561904463000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0240-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,22]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["240"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0240-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,22]]}}}