{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T10:15:59Z","timestamp":1772532959557,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,9,18]],"date-time":"2017-09-18T00:00:00Z","timestamp":1505692800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,9,18]]},"DOI":"10.1145\/3128473.3128475","type":"proceedings-article","created":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T12:27:52Z","timestamp":1504268872000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["From Statecharts into Model Checking"],"prefix":"10.1145","author":[{"given":"Valdivino Alexandre","family":"de Santiago J\u00fanior","sequence":"first","affiliation":[{"name":"Instituto Nacional de Pesquisas Espaciais (INPE), S\u00e3o Jos\u00e9 dos Campos, SP, Brazil"}]},{"given":"Felipe Elias Costa","family":"da Silva","sequence":"additional","affiliation":[{"name":"Instituto Nacional de Pesquisas Espaciais (INPE), S\u00e3o Jos\u00e9 dos Campos, SP, Brazil"}]}],"member":"320","published-online":{"date-parts":[[2017,9,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.1999.809499"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.6028\/NIST.IR.6166"},{"key":"e_1_3_2_1_3_1","volume-title":"Principles of model checking","author":"Baier C.","year":"2008","unstructured":"C. Baier and J.-P. Katoen . Principles of model checking . The MIT Press , Cambridge, MA, USA , 2008 . 975 p. C. Baier and J.-P. Katoen. Principles of model checking. The MIT Press, Cambridge, MA, USA, 2008. 975 p."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_36"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21410-8_39"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993288.2993289"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/CMPSAC.2002.1044538"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035401"},{"key":"e_1_3_2_1_10_1","first-page":"1","volume-title":"International Journal on Software Tools for Technology Transfer","author":"Enoiu E. P.","year":"2014","unstructured":"E. P. Enoiu , A. \u010cau\u0161evi\u0107 , T. J. Ostrand , E. J. Weyuker , D. Sundmark , and P. Pettersson . Automated test generation using model checking: an industrial evaluation . International Journal on Software Tools for Technology Transfer , pages 1 -- 19 , 2014 . E. P. Enoiu, A. \u010cau\u0161evi\u0107, T. J. Ostrand, E. J. Weyuker, D. Sundmark, and P. Pettersson. Automated test generation using model checking: an industrial evaluation. International Journal on Software Tools for Technology Transfer, pages 1--19, 2014."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAIC.PART.2007.30"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.402"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/318774.318939"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0059-8"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_3_2_1_16_1","first-page":"232","volume-title":"Proc. Int. Conf. Software Engineering (ICSE)","author":"Hong H. S.","year":"2003","unstructured":"H. S. Hong , S. D. Cha , I. Lee , O. Sokolsky , and H. Ural . Data flow testing as model checking . In Proc. Int. Conf. Software Engineering (ICSE) , pages 232 -- 242 . IEEE, 2003 . H. S. Hong, S. D. Cha, I. Lee, O. Sokolsky, and H. Ural. Data flow testing as model checking. In Proc. Int. Conf. Software Engineering (ICSE), pages 232--242. IEEE, 2003."},{"key":"e_1_3_2_1_17_1","volume-title":"Automatic test generation from statecharts using model checking. Technical report","author":"Hong H. S.","year":"2001","unstructured":"H. S. Hong , I. Lee , O. Sokolsky , and S. D. Cha . Automatic test generation from statecharts using model checking. Technical report , University of Pennsylvania , 2001 . H. S. Hong, I. Lee, O. Sokolsky, and S. D. Cha. Automatic test generation from statecharts using model checking. Technical report, University of Pennsylvania, 2001."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_23"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/PRDC.2009.15"},{"key":"e_1_3_2_1_20_1","first-page":"372","volume-title":"Proc. Int. Conf. Software Engineering (ICSE)","author":"Konrad S.","year":"2005","unstructured":"S. Konrad and B. H. C. Cheng . Real-time specification patterns . In Proc. Int. Conf. Software Engineering (ICSE) , pages 372 -- 381 . ACM, 2005 . S. Konrad and B. H. C. Cheng. Real-time specification patterns. In Proc. Int. Conf. Software Engineering (ICSE), pages 372--381. ACM, 2005."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2001.922409"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2001.966804"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-011-9155-6"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007526"}],"event":{"name":"SAST '17: 2nd Brazilian Symposium on Systematic and Automated Software Testing","location":"Fortaleza Brazil","acronym":"SAST '17","sponsor":["SBC Sociedade Brasileira de Computa\u00e7\u00e3o"]},"container-title":["Proceedings of the 2nd Brazilian Symposium on Systematic and Automated Software Testing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3128473.3128475","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3128473.3128475","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:01Z","timestamp":1750212661000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3128473.3128475"}},"subtitle":["A Hierarchy-based Translation and Specification Patterns Properties to Generate Test Cases"],"short-title":[],"issued":{"date-parts":[[2017,9,18]]},"references-count":24,"alternative-id":["10.1145\/3128473.3128475","10.1145\/3128473"],"URL":"https:\/\/doi.org\/10.1145\/3128473.3128475","relation":{},"subject":[],"published":{"date-parts":[[2017,9,18]]},"assertion":[{"value":"2017-09-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}