{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T05:13:58Z","timestamp":1778649238145,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,20]],"date-time":"2020-10-20T00:00:00Z","timestamp":1603152000000},"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":[[2020,10,20]]},"DOI":"10.1145\/3425174.3425213","type":"proceedings-article","created":{"date-parts":[[2020,10,23]],"date-time":"2020-10-23T00:01:25Z","timestamp":1603411285000},"page":"60-68","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Asserting Functional Equivalence between C Code and SCADE Models in Code-to-Model Transformations"],"prefix":"10.1145","author":[{"given":"Jan","family":"Toennemann","sequence":"first","affiliation":[{"name":"Institute for Software and Systems Engineering, TU Clausthal, Clausthal-Zellerfeld, Germany"}]},{"given":"Adina","family":"Anicul\u0103esei","sequence":"additional","affiliation":[{"name":"Institute for Software and Systems Engineering, TU Clausthal, Clausthal-Zellerfeld, Germany"}]},{"given":"Andreas","family":"Rausch","sequence":"additional","affiliation":[{"name":"Institute for Software and Systems Engineering, TU Clausthal, Clausthal-Zellerfeld, Germany"}]}],"member":"320","published-online":{"date-parts":[[2020,10,22]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Ch. Andr\u00e9. 1995. SyncCharts: A visual representation of reactive behaviors. Ch. Andr\u00e9. 1995. SyncCharts: A visual representation of reactive behaviors."},{"key":"e_1_3_2_1_2_1","first-page":"2","article-title":"On the Mutual Dependence Between Formal Methods and Empirical Testing in Program Verification","volume":"33","author":"Angius Nicola","year":"2019","unstructured":"Nicola Angius . 2019 . On the Mutual Dependence Between Formal Methods and Empirical Testing in Program Verification . Philosophy & Technology 33 , 2 (jul 2019), 349--355. https:\/\/doi.org\/10.1007\/s13347-019-00364-9 10.1007\/s13347-019-00364-9 Nicola Angius. 2019. On the Mutual Dependence Between Formal Methods and Empirical Testing in Program Verification. Philosophy & Technology 33, 2 (jul 2019), 349--355. https:\/\/doi.org\/10.1007\/s13347-019-00364-9","journal-title":"Philosophy & Technology"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/VST.2018.8327150"},{"key":"e_1_3_2_1_4_1","volume-title":"11th International Conference on Adaptive and Self-Adaptive Systems and Applications (ADAPTIVE","author":"Aniculaesei Adina","year":"2019","unstructured":"Adina Aniculaesei , Andreas Rausch , and Andreas Vorwald . 2019 . Automated Generation of Requirements-Based Test Cases for an Automotive Function using the SCADE Toolchain . In 11th International Conference on Adaptive and Self-Adaptive Systems and Applications (ADAPTIVE 2019). Adina Aniculaesei, Andreas Rausch, and Andreas Vorwald. 2019. Automated Generation of Requirements-Based Test Cases for an Automotive Function using the SCADE Toolchain. In 11th International Conference on Adaptive and Self-Adaptive Systems and Applications (ADAPTIVE 2019)."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/MODELS-C.2019.00079"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"G\u00e9rard Berry. 2000. The Foundations of Esterel. In Proof Language and Interaction: Essays in Honour of Robin Milner (2000-05-01) C. Stirling G. Plotkin and M. Tofte (Eds.). 425--454. G\u00e9rard Berry. 2000. The Foundations of Esterel. In Proof Language and Interaction: Essays in Honour of Robin Milner (2000-05-01) C. Stirling G. Plotkin and M. Tofte (Eds.). 425--454.","DOI":"10.7551\/mitpress\/5641.003.0021"},{"key":"e_1_3_2_1_7_1","volume-title":"The Esterel v5 Language Primer Version v5.91. (01","author":"Berry G\u00e9rard","year":"2004","unstructured":"G\u00e9rard Berry . 2004. The Esterel v5 Language Primer Version v5.91. (01 2004 ). G\u00e9rard Berry. 2004. The Esterel v5 Language Primer Version v5.91. (01 2004)."},{"key":"e_1_3_2_1_8_1","volume-title":"SCADE: Synchronous Design and Validation of Embedded Control Software. In Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems","author":"Berry G\u00e9rard","year":"2007","unstructured":"G\u00e9rard Berry . 2007 . SCADE: Synchronous Design and Validation of Embedded Control Software. In Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems , S. Ramesh and Prahladavaradan Sampath (Eds.). Springer Netherlands , Dordrecht , 19--33. G\u00e9rard Berry. 2007. SCADE: Synchronous Design and Validation of Embedded Control Software. In Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems, S. Ramesh and Prahladavaradan Sampath (Eds.). Springer Netherlands, Dordrecht, 19--33."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/RIVF.2008.4586365"},{"key":"e_1_3_2_1_10_1","first-page":"1","article-title":"Guiding requirements engineering for software-intensive embedded systems in the automotive industry","volume":"29","author":"Braun Peter","year":"2010","unstructured":"Peter Braun , Manfred Broy , Frank Houdek , Matthias Kirchmayr , Mark M\u00fcller , Birgit Penzenstadler , Klaus Pohl , and Thorsten Weyer . 2010 . Guiding requirements engineering for software-intensive embedded systems in the automotive industry . Computer Science - Research and Development 29 , 1 (oct 2010), 21--43. https:\/\/doi.org\/10.1007\/s00450-010-0136-y 10.1007\/s00450-010-0136-y Peter Braun, Manfred Broy, Frank Houdek, Matthias Kirchmayr, Mark M\u00fcller, Birgit Penzenstadler, Klaus Pohl, and Thorsten Weyer. 2010. Guiding requirements engineering for software-intensive embedded systems in the automotive industry. Computer Science - Research and Development 29, 1 (oct 2010), 21--43. https:\/\/doi.org\/10.1007\/s00450-010-0136-y","journal-title":"Computer Science - Research and Development"},{"key":"#cr-split#-e_1_3_2_1_11_1.1","doi-asserted-by":"crossref","unstructured":"Paul Caspi Grgoire Hamon and Marc Pouzet. 2008. Synchronous Functional Programming with Lucid Synchrone. In Modeling and Verification of Real-Time Systems. ISTE 207--247. https:\/\/doi.org\/10.1002\/9780470611012.ch7 10.1002\/9780470611012.ch7","DOI":"10.1002\/9780470611012.ch7"},{"key":"#cr-split#-e_1_3_2_1_11_1.2","doi-asserted-by":"crossref","unstructured":"Paul Caspi Grgoire Hamon and Marc Pouzet. 2008. Synchronous Functional Programming with Lucid Synchrone. In Modeling and Verification of Real-Time Systems. ISTE 207--247. https:\/\/doi.org\/10.1002\/9780470611012.ch7","DOI":"10.1002\/9780470611012.ch7"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2017.8285623"},{"key":"e_1_3_2_1_13_1","volume-title":"Systems & Structures 43 (oct","author":"da Silva Alberto Rodrigues","year":"2015","unstructured":"Alberto Rodrigues da Silva . 2015. Model-driven engineering: A survey supported by the unified conceptual model. Computer Languages , Systems & Structures 43 (oct 2015 ), 139--155. https:\/\/doi.org\/10.1016\/j.cl.2015.06.001 10.1016\/j.cl.2015.06.001 Alberto Rodrigues da Silva. 2015. Model-driven engineering: A survey supported by the unified conceptual model. Computer Languages, Systems & Structures 43 (oct 2015), 139--155. https:\/\/doi.org\/10.1016\/j.cl.2015.06.001"},{"key":"e_1_3_2_1_14_1","volume-title":"SCADE Suite User Manual","author":"Esterel Technologies S.A.S.","unstructured":"Esterel Technologies S.A.S. [n.d.]. SCADE Suite User Manual . ANSYS Inc . Esterel Technologies S.A.S. [n.d.]. SCADE Suite User Manual. ANSYS Inc."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/tse.2015.2421011"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1002\/bltj.2103"},{"key":"e_1_3_2_1_17_1","volume-title":"SPIN Model Checking and Software Verification","author":"Holzmann Gerard J.","unstructured":"Gerard J. Holzmann . 2000. Logic Verification of ANSI-C Code with SPIN . In SPIN Model Checking and Software Verification . Springer Berlin Heidelberg , 131--147. https:\/\/doi.org\/10.1007\/10722468_8 10.1007\/10722468_8 Gerard J. Holzmann. 2000. Logic Verification of ANSI-C Code with SPIN. In SPIN Model Checking and Software Verification. Springer Berlin Heidelberg, 131--147. https:\/\/doi.org\/10.1007\/10722468_8"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.228"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0026-2714(79)90360-3"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceeding of the 33rd international conference on Software engineering - ICSE '11. ACM Press. https:\/\/doi.org\/10","author":"Hutchinson John","year":"2011","unstructured":"John Hutchinson , Mark Rouncefield , and Jon Whittle . 2011 . Model-driven engineering practices in industry . In Proceeding of the 33rd international conference on Software engineering - ICSE '11. ACM Press. https:\/\/doi.org\/10 .1145\/1985793.1985882 10.1145\/1985793.1985882 John Hutchinson, Mark Rouncefield, and Jon Whittle. 2011. Model-driven engineering practices in industry. In Proceeding of the 33rd international conference on Software engineering - ICSE '11. ACM Press. https:\/\/doi.org\/10.1145\/1985793.1985882"},{"key":"e_1_3_2_1_21_1","first-page":"2","article-title":"Extracting models from source code in software modernization","volume":"13","author":"C\u00e1novas Izquierdo Javier Luis","year":"2012","unstructured":"Javier Luis C\u00e1novas Izquierdo and Jes\u00fas Garc\u00eda Molina . 2012 . Extracting models from source code in software modernization . Software & Systems Modeling 13 , 2 (sep 2012), 713--734. https:\/\/doi.org\/10.1007\/s10270-012-0270-z 10.1007\/s10270-012-0270-z Javier Luis C\u00e1novas Izquierdo and Jes\u00fas Garc\u00eda Molina. 2012. Extracting models from source code in software modernization. Software & Systems Modeling 13, 2 (sep 2012), 713--734. https:\/\/doi.org\/10.1007\/s10270-012-0270-z","journal-title":"Software & Systems Modeling"},{"key":"e_1_3_2_1_23_1","volume-title":"Model-Based Development of Software-intensive Automotive Systems. Dissertation. Technische Universit\u00e4t M\u00fcnchen","author":"Kugele Stefan","unstructured":"Stefan Kugele . 2012. Model-Based Development of Software-intensive Automotive Systems. Dissertation. Technische Universit\u00e4t M\u00fcnchen , M\u00fcnchen . https:\/\/mediatum.ub.tum.de\/node?id=1110104 Stefan Kugele. 2012. Model-Based Development of Software-intensive Automotive Systems. Dissertation. Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen. https:\/\/mediatum.ub.tum.de\/node?id=1110104"},{"key":"e_1_3_2_1_24_1","first-page":"2","article-title":"Software model checking takes off","volume":"53","author":"Miller Steven P.","year":"2010","unstructured":"Steven P. Miller , Michael W. Whalen , and Darren D. Cofer . 2010 . Software model checking takes off . Commun. ACM 53 , 2 (feb 2010), 58--64. https:\/\/doi.org\/10.1145\/1646353.1646372 10.1145\/1646353.1646372 Steven P. Miller, Michael W. Whalen, and Darren D. Cofer. 2010. Software model checking takes off. Commun. ACM 53, 2 (feb 2010), 58--64. https:\/\/doi.org\/10.1145\/1646353.1646372","journal-title":"Commun. ACM"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1155\/2007\/59130"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TEC.2019.2941175"},{"key":"e_1_3_2_1_27_1","volume-title":"Heimdahl","author":"Rajan Ajitha","year":"2008","unstructured":"Ajitha Rajan , Michael Whalen , Matt Staats , and Mats P. E . Heimdahl . 2008 . Requirements Coverage as an Adequacy Measure for Conformance Testing. In Formal Methods and Software Engineering. Springer Berlin Heidelberg , 86--104. https:\/\/doi.org\/10.1007\/978-3-540-88194-0_8 10.1007\/978-3-540-88194-0_8 Ajitha Rajan, Michael Whalen, Matt Staats, and Mats P. E. Heimdahl. 2008. Requirements Coverage as an Adequacy Measure for Conformance Testing. In Formal Methods and Software Engineering. Springer Berlin Heidelberg, 86--104. https:\/\/doi.org\/10.1007\/978-3-540-88194-0_8"},{"key":"e_1_3_2_1_28_1","volume-title":"Model Extraction of Legacy C Code in SCCharts. In 7th International Symposiumon Leveraging Applications of Formal Methods, Verification and Validation.","author":"Smyth Steven","year":"2016","unstructured":"Steven Smyth , Stephan Lenga , and Reinhard von Hanxelden . 2016 . Model Extraction of Legacy C Code in SCCharts. In 7th International Symposiumon Leveraging Applications of Formal Methods, Verification and Validation. Steven Smyth, Stephan Lenga, and Reinhard von Hanxelden. 2016. Model Extraction of Legacy C Code in SCCharts. In 7th International Symposiumon Leveraging Applications of Formal Methods, Verification and Validation."},{"key":"e_1_3_2_1_29_1","volume-title":"2013 35th International Conference on Software Engineering (ICSE). 102--111","author":"Whalen M.","unstructured":"M. Whalen , G. Gay , D. You , M. P. E. Heimdahl , and M. Staats . 2013. Observable modified condition\/decision coverage . In 2013 35th International Conference on Software Engineering (ICSE). 102--111 . M. Whalen, G. Gay, D. You, M. P. E. Heimdahl, and M. Staats. 2013. Observable modified condition\/decision coverage. In 2013 35th International Conference on Software Engineering (ICSE). 102--111."},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of International Symposium on Software Testing and Analysis. ACM, 25--36","author":"Whalen M.W","year":"2006","unstructured":"M.W Whalen , A. Rajan , and M.P.E. Heimdahl . 2006 . Coverage Metrics for Requirements-Based Testing . In Proceedings of International Symposium on Software Testing and Analysis. ACM, 25--36 . https:\/\/doi.org\/10.1145\/1146238.1146242 10.1145\/1146238.1146242 M.W Whalen, A. Rajan, and M.P.E. Heimdahl. 2006. Coverage Metrics for Requirements-Based Testing. In Proceedings of International Symposium on Software Testing and Analysis. ACM, 25--36. https:\/\/doi.org\/10.1145\/1146238.1146242"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2013.65"},{"key":"e_1_3_2_1_33_1","volume-title":"Empirical Software Engineering Issues. Critical Assessment and Future Directions","author":"Zelkowitz Marvin V.","unstructured":"Marvin V. Zelkowitz . 2007. Techniques for Empirical Validation . In Empirical Software Engineering Issues. Critical Assessment and Future Directions . Springer Berlin Heidelberg , 4--9. https:\/\/doi.org\/10.1007\/978-3-540-71301-2_2 10.1007\/978-3-540-71301-2_2 Marvin V. Zelkowitz. 2007. Techniques for Empirical Validation. In Empirical Software Engineering Issues. Critical Assessment and Future Directions. Springer Berlin Heidelberg, 4--9. https:\/\/doi.org\/10.1007\/978-3-540-71301-2_2"}],"event":{"name":"SAST 20: 5th Brazilian Symposium on Systematic and Automated Software Testing","location":"Natal Brazil","acronym":"SAST 20","sponsor":["SBC Brazilian Computer Society"]},"container-title":["Proceedings of the 5th Brazilian Symposium on Systematic and Automated Software Testing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3425174.3425213","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3425174.3425213","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:54Z","timestamp":1750195914000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3425174.3425213"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,20]]},"references-count":32,"alternative-id":["10.1145\/3425174.3425213","10.1145\/3425174"],"URL":"https:\/\/doi.org\/10.1145\/3425174.3425213","relation":{},"subject":[],"published":{"date-parts":[[2020,10,20]]},"assertion":[{"value":"2020-10-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}