{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T11:47:27Z","timestamp":1725450447295},"reference-count":38,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,9]]},"DOI":"10.1109\/fdl.2018.8524044","type":"proceedings-article","created":{"date-parts":[[2018,11,8]],"date-time":"2018-11-08T23:21:35Z","timestamp":1541719295000},"page":"5-16","source":"Crossref","is-referenced-by-count":0,"title":["Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code"],"prefix":"10.1109","author":[{"given":"Guillaume","family":"Davy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Garion","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre- Loic","family":"Garoche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Roux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Thirioux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61648-9_53"},{"key":"ref33","first-page":"132","article-title":"A non-linear arithmetic procedure for control-command software verification","author":"roux","year":"2018","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems ? 24th International Conference TACAS 2018 ETAPS 2018 Thessaloniki Greece April 14–20 2018 Proceedings Part II"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9339-z"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2015.2465571"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6911(95)00063-1"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883824"},{"key":"ref36","first-page":"1","article-title":"The versatile synchronous observer","author":"rushby","year":"2012","journal-title":"SBMF"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/s10543-006-0056-1"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728623"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_1"},{"key":"ref11","first-page":"178","article-title":"Lustre: A declarative language for programming synchronous systems","author":"caspi","year":"1987","journal-title":"POPL"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"journal-title":"CENELEC 50128 - Railway applications - Communication signalling and processing systems - Software for railway control and protection systems","year":"2001","key":"ref13"},{"key":"ref14","first-page":"126","article-title":"Compositional verification of architectural models","author":"cofer","year":"2012","journal-title":"NASA Formal Methods-4th International Symposium NFM 2012"},{"key":"ref15","first-page":"233","article-title":"Frama-c: a software analysis perspective","author":"cuoq","year":"2012","journal-title":"SEFM'12"},{"journal-title":"DO-178C Software Considerations in Airborne Systems and Equipment Certification","year":"2011","key":"ref16"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.169.4"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"ref19","doi-asserted-by":"crossref","first-page":"1305","DOI":"10.1109\/5.97300","article-title":"The synchronous dataflow programming language lustre","author":"halbwachs","year":"1991","journal-title":"Proceedings of the IEEE"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596582"},{"journal-title":"ACSL ANSI\/ISO C Specification Language Version 1 5","year":"0","author":"baudin","key":"ref4"},{"journal-title":"Interior-point Polynomial Algorithms in Convex Programming volume 13 of Studies in Applied Mathematics Society for Industrial and Applied Mathematics","year":"1994","author":"nesterov","key":"ref27"},{"key":"ref3","doi-asserted-by":"crossref","DOI":"10.1515\/9781400828739","author":"astrom","year":"2008","journal-title":"Feedback Systems An Introduction for Scientists and Engineers"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"ref29","first-page":"151","article-title":"Translation validation","author":"pnueli","year":"1998","journal-title":"Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems TACAS '98"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/5.97297"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062358"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1375657.1375674"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/207110.207134"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804441"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2017.03.001"},{"key":"ref20","first-page":"83","article-title":"Synchronous observers and the verification of reactive systems","author":"halbwachs","year":"1993","journal-title":"AMAST"},{"key":"ref22","article-title":"Certifying an automated code generator using formal tools: Preliminary experiments in the geneauto project","author":"izerrouken","year":"2008","journal-title":"European Congress on Embedded Real-Time Software (ERTS) Toulouse 2910112008–0110212008"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.72.6"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"ref25","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1145\/358438.349314","article-title":"Translation validation for an optimizing compiler","author":"necula","year":"2000","journal-title":"SIGPLAN Not"}],"event":{"name":"2018 Forum on specification & Design Languages (FDL)","start":{"date-parts":[[2018,9,10]]},"location":"Garching","end":{"date-parts":[[2018,9,12]]}},"container-title":["2018 Forum on Specification & Design Languages (FDL)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8501260\/8524032\/08524044.pdf?arnumber=8524044","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T21:25:30Z","timestamp":1643232330000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8524044\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9]]},"references-count":38,"URL":"https:\/\/doi.org\/10.1109\/fdl.2018.8524044","relation":{},"subject":[],"published":{"date-parts":[[2018,9]]}}}