{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,21]],"date-time":"2026-04-21T15:14:47Z","timestamp":1776784487508,"version":"3.51.2"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2021,7,29]],"date-time":"2021-07-29T00:00:00Z","timestamp":1627516800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANR JCJC FEANICSES","award":["ANR-17-CE25-0018"],"award-info":[{"award-number":["ANR-17-CE25-0018"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2021,7,31]]},"abstract":"<jats:p>Model-based design is now unavoidable when building embedded systems and, more specifically, controllers. Among the available model languages, the synchronous dataflow paradigm, as implemented in languages such as MATLAB Simulink or ANSYS SCADE, has become predominant in critical embedded system industries. Both of these frameworks are used to design the controller itself but also provide code generation means, enabling faster deployment to target and easier V&amp;V activities performed earlier in the design process, at the model level. Synchronous models also ease the definition of formal specification through the use of synchronous observers, attaching requirements to the model in the very same language, mastered by engineers and tooled with simulation means or code generation.<\/jats:p>\n          <jats:p>However, few works address the automatic synthesis of MATLAB Simulink annotations from lower-level models or code. This article presents a compilation process from Lustre models to genuine MATLAB Simulink, without the need to rely on external C functions or MATLAB functions. This translation is based on the modular compilation of Lustre to imperative code and preserves the hierarchy of the input Lustre model within the generated Simulink one. We implemented the approach and used it to validate a compilation toolchain, mapping Simulink to Lustre and then C, thanks to equivalence testing and checking. This backward compilation from Lustre to Simulink also provides the ability to produce automatically Simulink components modeling specification, proof arguments, or test cases coverage criteria.<\/jats:p>","DOI":"10.1145\/3461668","type":"journal-article","created":{"date-parts":[[2021,7,29]],"date-time":"2021-07-29T17:32:45Z","timestamp":1627579965000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["From Lustre to Simulink"],"prefix":"10.1145","volume":"5","author":[{"given":"Hamza","family":"Bourbouh","sequence":"first","affiliation":[{"name":"KBR\/NASA Ames Research Center, Mountain View, CA"}]},{"given":"Pierre-Lo\u00efc","family":"Garoche","sequence":"additional","affiliation":[{"name":"KBR\/NASA Ames Research Center\/ENAC, Universit\u00e9 de Toulouse, Toulouse, France"}]},{"given":"Christophe","family":"Garion","sequence":"additional","affiliation":[{"name":"ISAE-SUPAERO, Universit\u00e9 de Toulouse, Toulouse, France"}]},{"given":"Xavier","family":"Thirioux","sequence":"additional","affiliation":[{"name":"ISAE-SUPAERO, Universit\u00e9 de Toulouse, Toulouse, France"}]}],"member":"320","published-online":{"date-parts":[[2021,7,29]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"RTCA. 2011. DO-178C. Software Considerations in Airborne Systems and Equipment Certification. RTCA.  RTCA. 2011. DO-178C. Software Considerations in Airborne Systems and Equipment Certification. RTCA."},{"key":"e_1_2_1_2_1","volume-title":"SPARK 2014 Reference Manual. Retrieved","author":"Ltd AdaCore","year":"2020","unstructured":"AdaCore and Altran UK Ltd . 2020 . SPARK 2014 Reference Manual. Retrieved June 3, 2021 from http:\/\/docs.adacore.com\/spark2014-docs\/html\/lrm\/. AdaCore and Altran UK Ltd. 2020. SPARK 2014 Reference Manual. Retrieved June 3, 2021 from http:\/\/docs.adacore.com\/spark2014-docs\/html\/lrm\/."},{"key":"e_1_2_1_3_1","first-page":"16","article-title":"ACSL: ANSI\/ISO C Specification Language","volume":"1","author":"Baudin Patrick","year":"2020","unstructured":"Patrick Baudin , Pascal Cuoq , Jean-Christophe Filli\u00e2tre , Claude March\u00e9 , Benjamin Monate , Yannick Moy , and Virgile Prevosto . 2020 . ACSL: ANSI\/ISO C Specification Language , Version 1 . 16 . Retrieved June 3, 2021 from https:\/\/www.frama-c.com\/download\/acsl.pdf. Patrick Baudin, Pascal Cuoq, Jean-Christophe Filli\u00e2tre, Claude March\u00e9, Benjamin Monate, Yannick Moy, and Virgile Prevosto. 2020. ACSL: ANSI\/ISO C Specification Language, Version 1.16. Retrieved June 3, 2021 from https:\/\/www.frama-c.com\/download\/acsl.pdf.","journal-title":"Version"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375657.1375674"},{"key":"e_1_2_1_6_1","volume-title":"n.d. CoCoSim\u2014Automated Analysis Framework for Simulink. Retrieved","author":"Bourbouh Hamza","year":"2021","unstructured":"Hamza Bourbouh . n.d. CoCoSim\u2014Automated Analysis Framework for Simulink. Retrieved June 3, 2021 from https:\/\/github.com\/NASA-SW-VnV\/CoCoSim. Hamza Bourbouh. n.d. CoCoSim\u2014Automated Analysis Framework for Simulink. Retrieved June 3, 2021 from https:\/\/github.com\/NASA-SW-VnV\/CoCoSim."},{"key":"e_1_2_1_7_1","volume-title":"21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning","volume":"46","author":"Bourbouh Hamza","year":"2017","unstructured":"Hamza Bourbouh , Pierre-Lo\u00efc Garoche , Christophe Garion , Arie Gurfinkel , Temesghen Kahsai , and Xavier Thirioux . 2017 . Automated analysis of Stateflow models. In LPAR-21 , 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning , Maun, Botswana , May 7-12, 2017.EPiC Series in Computing, Thomas Eiter and David Sands (Eds.), Vol. 46 . EasyChair, 144\u2013161. http:\/\/www.easychair.org\/publications\/paper\/340361. Hamza Bourbouh, Pierre-Lo\u00efc Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai, and Xavier Thirioux. 2017. Automated analysis of Stateflow models. In LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017.EPiC Series in Computing, Thomas Eiter and David Sands (Eds.), Vol. 46. EasyChair, 144\u2013161. http:\/\/www.easychair.org\/publications\/paper\/340361."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 10th European Congress on Embedded Real Time Software and Systems (ERTS\u201920)","author":"Bourbouh Hamza","year":"2020","unstructured":"Hamza Bourbouh , Pierre-Lo\u00efc Garoche , Thomas Loquen , \u00c9ric Noulard , and Claire Pagetti . 2020 . CoCoSim, a code generation framework for control\/command applications: An overview of CoCoSim for multi-periodic discrete Simulink models . In Proceedings of the 10th European Congress on Embedded Real Time Software and Systems (ERTS\u201920) . Hamza Bourbouh, Pierre-Lo\u00efc Garoche, Thomas Loquen, \u00c9ric Noulard, and Claire Pagetti. 2020. CoCoSim, a code generation framework for control\/command applications: An overview of CoCoSim for multi-periodic discrete Simulink models. In Proceedings of the 10th European Congress on Embedded Real Time Software and Systems (ERTS\u201920)."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062358"},{"key":"e_1_2_1_10_1","series-title":"Lecture Notes in Computer Science","volume-title":"FM 2015: Formal Methods","author":"Brat Guillaume","unstructured":"Guillaume Brat , David H. Bushnell , Misty Davies , Dimitra Giannakopoulou , Falk Howar , and Temesghen Kahsai . 2015. Verifying the safety of a flight-critical system . In FM 2015: Formal Methods . Lecture Notes in Computer Science , Vol. 9109 . Springer , 308\u2013324. DOI:https:\/\/doi.org\/10.1007\/978-3-319-19249-9_20 10.1007\/978-3-319-19249-9_20 Guillaume Brat, David H. Bushnell, Misty Davies, Dimitra Giannakopoulou, Falk Howar, and Temesghen Kahsai. 2015. Verifying the safety of a flight-critical system. In FM 2015: Formal Methods. Lecture Notes in Computer Science, Vol. 9109. Springer, 308\u2013324. DOI:https:\/\/doi.org\/10.1007\/978-3-319-19249-9_20"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"key":"e_1_2_1_12_1","series-title":"Lecture Notes in Computer Science","volume-title":"Software Engineering and Formal Methods","author":"Champion Adrien","unstructured":"Adrien Champion , Arie Gurfinkel , Temesghen Kahsai , and Cesare Tinelli . 2016. CoCoSpec: A mode-aware contract language for reactive systems . In Software Engineering and Formal Methods . Lecture Notes in Computer Science , Vol. 9763 . Springer , 347\u2013366. DOI:https:\/\/doi.org\/10.1007\/978-3-319-41591-8_24 10.1007\/978-3-319-41591-8_24 Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, and Cesare Tinelli. 2016. CoCoSpec: A mode-aware contract language for reactive systems. In Software Engineering and Formal Methods. Lecture Notes in Computer Science, Vol. 9763. Springer, 347\u2013366. DOI:https:\/\/doi.org\/10.1007\/978-3-319-41591-8_24"},{"key":"e_1_2_1_13_1","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"Champion Adrien","unstructured":"Adrien Champion , Alain Mebsout , Christoph Sticksel , and Cesare Tinelli . 2016. The Kind 2 model checker . In Computer Aided Verification . Lecture Notes in Computer Science , Vol. 9780 . Springer , 510\u2013517. DOI:https:\/\/doi.org\/10.1007\/978-3-319-41540-6_29 10.1007\/978-3-319-41540-6_29 Adrien Champion, Alain Mebsout, Christoph Sticksel, and Cesare Tinelli. 2016. The Kind 2 model checker. In Computer Aided Verification. Lecture Notes in Computer Science, Vol. 9780. Springer, 510\u2013517. DOI:https:\/\/doi.org\/10.1007\/978-3-319-41540-6_29"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEAA.2012.68"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086261"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2695664.2695819"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 2016 Safe and Secure Systems and Software Symposium (S5\u201916)","author":"Elliott Chris","year":"2016","unstructured":"Chris Elliott . 2016 . An example set of cyber-physical V&V challenges for S5, Lockheed Martin Skunk works . In Proceedings of the 2016 Safe and Secure Systems and Software Symposium (S5\u201916) . http:\/\/mys5.org\/Proceedings\/2016\/Day_2\/2016-S5-Day2_0945_Elliott.pdf. Chris Elliott. 2016. An example set of cyber-physical V&V challenges for S5, Lockheed Martin Skunk works. In Proceedings of the 2016 Safe and Secure Systems and Software Symposium (S5\u201916). http:\/\/mys5.org\/Proceedings\/2016\/Day_2\/2016-S5-Day2_0945_Elliott.pdf."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 2015 Safe and Secure Systems and Software Symposium (S5\u201915)","author":"Elliott Chris","year":"2015","unstructured":"Chris Elliott . 2015 . On example models and challenges ahead for the evaluation of complex cyber-physical systems with state of the art formal methods V&V, Lockheed Martin Skunk works . In Proceedings of the 2015 Safe and Secure Systems and Software Symposium (S5\u201915) . http:\/\/mys5.org\/Proceedings\/2015\/Day_1\/2015-S5-Day1_1405_Elliott.pdf. Chris Elliott. 2015. On example models and challenges ahead for the evaluation of complex cyber-physical systems with state of the art formal methods V&V, Lockheed Martin Skunk works. In Proceedings of the 2015 Safe and Secure Systems and Software Symposium (S5\u201915). http:\/\/mys5.org\/Proceedings\/2015\/Day_1\/2015-S5-Day1_1405_Elliott.pdf."},{"key":"e_1_2_1_19_1","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"Gacek Andrew","unstructured":"Andrew Gacek , John Backes , Mike Whalen , Lucas G. Wagner , and Elaheh Ghassabani . 2018. The JKind model checker . In Computer Aided Verification . Lecture Notes in Computer Science , Vol. 10982 . Springer , 20\u201327. DOI:https:\/\/doi.org\/10.1007\/978-3-319-96142-2_3 10.1007\/978-3-319-96142-2_3 Andrew Gacek, John Backes, Mike Whalen, Lucas G. Wagner, and Elaheh Ghassabani. 2018. The JKind model checker. In Computer Aided Verification. Lecture Notes in Computer Science, Vol. 10982. Springer, 20\u201327. DOI:https:\/\/doi.org\/10.1007\/978-3-319-96142-2_3"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.169.4"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.219.2"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_19"},{"key":"e_1_2_1_23_1","series-title":"Lecture Notes in Computer Science","volume-title":"Requirements Engineering: Foundation for Software Quality","author":"Giannakopoulou Dimitra","unstructured":"Dimitra Giannakopoulou , Thomas Pressburger , Anastasia Mavridou , and Johann Schumann . 2020. Generation of formal requirements from structured natural language . In Requirements Engineering: Foundation for Software Quality . Lecture Notes in Computer Science , Vol. 12045 . Springer , 19\u201335. Dimitra Giannakopoulou, Thomas Pressburger, Anastasia Mavridou, and Johann Schumann. 2020. Generation of formal requirements from structured natural language. In Requirements Engineering: Foundation for Software Quality. Lecture Notes in Computer Science, Vol. 12045. Springer, 19\u201335."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the IEEE79","author":"Halbwachs N.","year":"1991","unstructured":"N. Halbwachs , P. Caspi , P. Raymond , and D. Pilaud . 1991. The synchronous dataflow programming language LUSTRE . Proceedings of the IEEE79 , 9 ( 1991 ), 1305\u20131320. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. 1991. The synchronous dataflow programming language LUSTRE. Proceedings of the IEEE79, 9 (1991), 1305\u20131320."},{"key":"e_1_2_1_25_1","volume-title":"Workshops in Computing. Springer, 83\u201396","author":"Halbwachs Nicolas","year":"1993","unstructured":"Nicolas Halbwachs , Fabienne Lagnier , and Pascal Raymond . 1993 . Synchronous observers and the verification of reactive systems. In Algebraic Methodology and Software Technology (AMAST\u201993) . Workshops in Computing. Springer, 83\u201396 . Nicolas Halbwachs, Fabienne Lagnier, and Pascal Raymond. 1993. Synchronous observers and the verification of reactive systems. In Algebraic Methodology and Software Technology (AMAST\u201993). Workshops in Computing. Springer, 83\u201396."},{"key":"e_1_2_1_26_1","series-title":"Lecture Notes in Computer Science","volume-title":"Advances in Computing Science\u2014ASIAN\u201999","author":"Halbwachs Nicolas","unstructured":"Nicolas Halbwachs and Pascal Raymond . 1999. Validation of synchronous reactive systems: From formal verification to automatic testing . In Advances in Computing Science\u2014ASIAN\u201999 . Lecture Notes in Computer Science , Vol. 1742 . Springer , 1\u201312. DOI:https:\/\/doi.org\/10.1007\/3-540-46674-6_1 10.1007\/3-540-46674-6_1 Nicolas Halbwachs and Pascal Raymond. 1999. Validation of synchronous reactive systems: From formal verification to automatic testing. In Advances in Computing Science\u2014ASIAN\u201999. Lecture Notes in Computer Science, Vol. 1742. Springer, 1\u201312. DOI:https:\/\/doi.org\/10.1007\/3-540-46674-6_1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.72.6"},{"key":"e_1_2_1_29_1","volume-title":"Whalen","author":"Katis Andreas","year":"2016","unstructured":"Andreas Katis , Grigory Fedyukovich , Andrew Gacek , John D. Backes , Arie Gurfinkel , and Michael W . Whalen . 2016 . Synthesis from assume-guarantee contracts using skolemized proofs of realizability. arXiv:1610.05867. Andreas Katis, Grigory Fedyukovich, Andrew Gacek, John D. Backes, Arie Gurfinkel, and Michael W. Whalen. 2016. Synthesis from assume-guarantee contracts using skolemized proofs of realizability. arXiv:1610.05867."},{"key":"e_1_2_1_30_1","series-title":"Lecture Notes in Computer Science","volume-title":"Hardware and Software: Verification and Testing","author":"Klein Uri","unstructured":"Uri Klein and Amir Pnueli . 2010. Revisiting synthesis of GR(1) specifications . In Hardware and Software: Verification and Testing . Lecture Notes in Computer Science , Vol. 6504 . Springer , 161\u2013181. DOI:https:\/\/doi.org\/10.1007\/978-3-642-19583-9_16 10.1007\/978-3-642-19583-9_16 Uri Klein and Amir Pnueli. 2010. Revisiting synthesis of GR(1) specifications. In Hardware and Software: Verification and Testing. Lecture Notes in Computer Science, Vol. 6504. Springer, 161\u2013181. DOI:https:\/\/doi.org\/10.1007\/978-3-642-19583-9_16"},{"key":"e_1_2_1_31_1","series-title":"Lecture Notes in Computer Science","volume-title":"NASA Formal Methods","author":"Liu Jing","unstructured":"Jing Liu , John D. Backes , Darren Cofer , and Andrew Gacek . 2016. From design contracts to component requirements verification . In NASA Formal Methods . Lecture Notes in Computer Science , Vol. 9690 . Springer , 373\u2013387. DOI:https:\/\/doi.org\/10.1007\/978-3-319-40648-0_28 10.1007\/978-3-319-40648-0_28 Jing Liu, John D. Backes, Darren Cofer, and Andrew Gacek. 2016. From design contracts to component requirements verification. In NASA Formal Methods. Lecture Notes in Computer Science, Vol. 9690. Springer, 373\u2013387. DOI:https:\/\/doi.org\/10.1007\/978-3-319-40648-0_28"},{"key":"e_1_2_1_32_1","unstructured":"Mathworks Inc. 2018. MATLAB Simulink (R2018b). Mathworks Inc. Natick MA.  Mathworks Inc. 2018. MATLAB Simulink (R2018b). Mathworks Inc. Natick MA."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2014.6926012"},{"key":"e_1_2_1_35_1","series-title":"Lecture Notes in Computer Science","volume-title":"Specification, Algebra, and Software","author":"Rushby John","unstructured":"John Rushby . 2014. The versatile synchronous observer . In Specification, Algebra, and Software . Lecture Notes in Computer Science , Vol. 8373 . Springer , 110\u2013128. John Rushby. 2014. The versatile synchronous observer. In Specification, Algebra, and Software. Lecture Notes in Computer Science, Vol. 8373. Springer, 110\u2013128."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017753.1017795"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1113830.1113834"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2012.173"}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3461668","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3461668","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:49:05Z","timestamp":1750193345000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3461668"}},"subtitle":["Reverse Compilation for Embedded Systems Applications"],"short-title":[],"issued":{"date-parts":[[2021,7,29]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,7,31]]}},"alternative-id":["10.1145\/3461668"],"URL":"https:\/\/doi.org\/10.1145\/3461668","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,29]]},"assertion":[{"value":"2020-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-07-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}