{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T17:53:57Z","timestamp":1774374837449,"version":"3.50.1"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2014,11,21]],"date-time":"2014-11-21T00:00:00Z","timestamp":1416528000000},"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":[[2016,6]]},"DOI":"10.1007\/s10009-014-0355-9","type":"journal-article","created":{"date-parts":[[2014,11,21]],"date-time":"2014-11-21T11:55:25Z","timestamp":1416570925000},"page":"335-353","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":42,"title":["Automated test generation using model checking: an industrial evaluation"],"prefix":"10.1007","volume":"18","author":[{"given":"Eduard P.","family":"Enoiu","sequence":"first","affiliation":[]},{"given":"Adnan","family":"\u010cau\u0161evi\u0107","sequence":"additional","affiliation":[]},{"given":"Thomas J.","family":"Ostrand","sequence":"additional","affiliation":[]},{"given":"Elaine J.","family":"Weyuker","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Sundmark","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Pettersson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,11,21]]},"reference":[{"key":"355_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R.: Timed automata. In: Computer aided verification, pp. 688\u2013688. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48683-6_3"},{"issue":"1","key":"355_CR2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2\u201334 (1993)","journal-title":"Inf. Comput."},{"key":"355_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.: Automata for modeling real-time systems. Autom. Lang. Progr. pp. 322\u2013335 (1990)","DOI":"10.1007\/BFb0032042"},{"key":"355_CR4","unstructured":"Ammann, P., Black, P.E., Ding, W.: Model checkers in software testing. In: NIST-IR 6777, National Institute of Standards and Technology Report (2002)"},{"key":"355_CR5","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511809163","volume-title":"Introduction to Software Testing","author":"P Ammann","year":"2008","unstructured":"Ammann, P., Offutt, J.: Introduction to Software Testing. Cambridge University Press, Cambridge (2008)"},{"key":"355_CR6","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G, Petterson, P., Romijn, J.: Guiding and cost-optimality in uppaal. In: AAAI-Spring Symposium on Model-based Validation of Intelligence, pp. 66\u201374 (2001)","DOI":"10.7146\/brics.v8i4.20458"},{"key":"355_CR7","doi-asserted-by":"crossref","unstructured":"Black, P.: Modeling and marshaling: making tests from model checker counter-examples. In: Proceedings of the 19th digital avionics systems conference, vol. 1, pp. 1B3-1. IEEE Press, New York (2000)","DOI":"10.1109\/DASC.2000.886880"},{"key":"355_CR8","unstructured":"CENELEC. 50128: Railway application-communications, signaling and processing systems-software for railway control and protection systems. Standard Report (2001)"},{"issue":"5","key":"355_CR9","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1049\/sej.1994.0025","volume":"9","author":"JJ Chilenski","year":"1994","unstructured":"Chilenski, J.J., Miller, S.P.: Applicability of modified condition\/decision coverage to software testing. Softw. Eng. J. 9(5), 193\u2013200 (1994)","journal-title":"Softw. Eng. J."},{"issue":"1","key":"355_CR10","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/S0304-3975(00)00089-X","volume":"253","author":"H Dierks","year":"2001","unstructured":"Dierks, H.: Plc-automata: a new class of implementable real-time automata. Theor. Comput. Sci. 253(1), 61\u201393 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"355_CR11","doi-asserted-by":"crossref","unstructured":"Enoiu, E.P., Sundmark, D., Pettersson, P.: Model-based test suite generation for function block diagrams using the UPPAAL model checker. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pp. 158\u2013167. IEEE Press, New York (2013)","DOI":"10.1109\/ICSTW.2013.27"},{"key":"355_CR12","doi-asserted-by":"crossref","unstructured":"Enoiu, E.P., Sundmark, D., Pettersson, P.: Using logic coverage to improve testing function block diagrams. In: Testing Software and Systems, pp. 1\u201316. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-41707-8_1"},{"key":"355_CR13","doi-asserted-by":"crossref","unstructured":"Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. In: Journal on Software Testing, Verification and Reliability, vol. 19, pp. 215\u2013261. Wiley Online Library, New York (2009)","DOI":"10.1002\/stvr.402"},{"key":"355_CR14","doi-asserted-by":"crossref","unstructured":"Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. In: Software Engineering, ESEC\/FSE99, pp. 146\u2013162. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48166-4_10"},{"key":"355_CR15","doi-asserted-by":"crossref","unstructured":"Hessel, A., Larsen, K., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. Form. Methods Test. pp. 77\u2013117 (2008)","DOI":"10.1007\/978-3-540-78917-8_3"},{"key":"355_CR16","doi-asserted-by":"crossref","unstructured":"Hessel, A., Larsen, K., Nielsen, B., Pettersson, P., Skou, A.: Time-optimal real-time test case generation using UPPAAL. In: Lecture notes in computer science. Formal approaches to software testing, pp. 114\u2013130. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24617-6_9"},{"key":"355_CR17","doi-asserted-by":"crossref","unstructured":"Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic-based theory of test coverage and generation. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 327\u2013341. Springer, Berlin (2002)","DOI":"10.1007\/3-540-46002-0_23"},{"key":"355_CR18","doi-asserted-by":"crossref","unstructured":"Jee, E., Kim, S., Cha, S., Lee, I.: Automated test coverage measurement for reactor protection system software implemented in function block diagram. In: Journal on Computer Safety, Reliability, and Security, pp. 223\u2013236. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-15651-9_17"},{"issue":"7","key":"355_CR19","doi-asserted-by":"crossref","first-page":"1131","DOI":"10.1016\/j.infsof.2009.01.003","volume":"51","author":"E Jee","year":"2009","unstructured":"Jee, E., Yoo, J., Cha, S., Bae, D.: A data flow-based structural testing technique for FBD programs. Inf. Softw. Technol. 51(7), 1131\u20131139 (2009)","journal-title":"Inf. Softw. Technol."},{"key":"355_CR20","doi-asserted-by":"crossref","unstructured":"Khurshid, S., P\u0103s\u0103reanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 553\u2013568. Springer, Berlin (2003)","DOI":"10.1007\/3-540-36577-X_40"},{"key":"355_CR21","doi-asserted-by":"crossref","unstructured":"Lakehal, A., Parissis, I.: Lustructu: a tool for the automatic coverage assessment of lustre programs. In: International Symposium on Software Reliability Engineering, p. 10. IEEE Press, New York (2005)","DOI":"10.1109\/ISSRE.2005.26"},{"issue":"1","key":"355_CR22","doi-asserted-by":"crossref","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. Int. J.Softw. Tools Technol. Transf. 1(1), 134\u2013152 (1997)","journal-title":"Int. J.Softw. Tools Technol. Transf."},{"key":"355_CR23","doi-asserted-by":"crossref","unstructured":"\u00d6hman, M., Johansson, S., \u00c5rz\u00e9n, K.E.: Implementation aspects of the PLC standard IEC 1131\u20133. In: Journal on Control Engineering Practice, vol. 6, pp. 547\u2013555. Elsevier, New York (1998)","DOI":"10.1016\/S0967-0661(98)00054-9"},{"key":"355_CR24","doi-asserted-by":"crossref","unstructured":"Rayadurgam, S., Heimdahl, M.P.E.: Generating MC\/DC adequate test sequences through model checking. In: NASA Goddard Software Engineering Workshop Proceedings, pp. 91\u201396. IEEE Press, New York (2003)","DOI":"10.1109\/SEW.2003.1270730"},{"key":"355_CR25","doi-asserted-by":"crossref","unstructured":"Rayadurgam, S., Heimdahl, M.P.E.: Coverage based test-case generation using model checkers. In: ECBS 2001. Proceedings of Eighth Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems, pp. 83\u201391. IEEE Press, New York (2001)","DOI":"10.1109\/ECBS.2001.922409"},{"key":"355_CR26","unstructured":"Seppi, K., Jones, M., Lamborn, P.: Guided model checking with a bayesian meta-heuristic. Fundam. Inf. 70(1), 111\u2013126 (2006)"},{"key":"355_CR27","doi-asserted-by":"crossref","unstructured":"Thieme, J., Hanisch, H.M.: Model-based generation of modular PLC code using IEC61131 function blocks. In: Proceedings of the International Symposium on Industrial Electronics, vol. 1, pp. 199\u2013204. IEEE Press, New York (2002)","DOI":"10.1109\/ISIE.2002.1026065"},{"key":"355_CR28","doi-asserted-by":"crossref","unstructured":"Whalen, M., Gay, G., You, D., Heimdahl, M.P.E., Staats, M.: Observable modified condition\/decision coverage. In: Proceedings of the International Conference on Software Engineering, pp. 102\u2013111. IEEE Press, New York (2013)","DOI":"10.1109\/ICSE.2013.6606556"}],"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-0355-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0355-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0355-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T20:09:07Z","timestamp":1747166947000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0355-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,21]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["355"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0355-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,21]]}}}