{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T10:31:16Z","timestamp":1749033076537},"reference-count":27,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,7]]},"DOI":"10.1109\/ecc.2015.7330941","type":"proceedings-article","created":{"date-parts":[[2015,11,23]],"date-time":"2015-11-23T22:45:17Z","timestamp":1448318717000},"page":"2670-2675","source":"Crossref","is-referenced-by-count":15,"title":["Verification of control systems implemented in simulink with assertion checks and theorem proving: A case study"],"prefix":"10.1109","author":[{"given":"Dejanira","family":"Araiza-Illan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kerstin","family":"Eder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arthur","family":"Richards","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"journal-title":"Prover Prover plug-in","year":"0","key":"ref10"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/ICFEM.2000.873817"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2006.1690376"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-011-0145-4"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT.2013.6658587"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/CONTROL.2014.6915147"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_8"},{"key":"ref17","article-title":"Bernstein-based polynomial approach to study the stability of switched systems and formal verification using HOL Light","author":"michael","year":"2014","journal-title":"arXiv 141 0 3969"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_15"},{"journal-title":"The Why3 Platform","year":"2013","author":"bobot","key":"ref19"},{"key":"ref4","first-page":"51","article-title":"Automated structural testing of SimulinkiTargetLink models via search-based testing assisted by prior-search static analysis","author":"wilmes","year":"2012","journal-title":"Proc of VALID"},{"journal-title":"The MathWorks","year":"2012","key":"ref27"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2007.05.039"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"ref6"},{"key":"ref5","article-title":"Set-based simulation for design and verification of Simulink models","author":"bouissou","year":"2014","journal-title":"Proc ERTS"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0195-3"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2002.806655"},{"key":"ref2","article-title":"GPS-based real-time navigation for the PRISMA formation flying mission","author":"d'amico","year":"2006","journal-title":"Proc NAVITEC"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32469-7_6"},{"key":"ref1","doi-asserted-by":"crossref","first-page":"606","DOI":"10.1007\/11901433_33","article-title":"Tool for translating Simulink models into input language of a model checker","author":"meenakshi","year":"2006","journal-title":"Formal Methods and Software Engineering"},{"journal-title":"Feedback Control of Dynamic Systems","year":"2011","author":"franklin","key":"ref20"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-0302-6"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/1879021.1879024"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1155\/2014\/201214"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.2478\/v10037-006-0004-1"},{"year":"0","key":"ref26"},{"year":"0","key":"ref25"}],"event":{"name":"2015 European Control Conference (ECC)","start":{"date-parts":[[2015,7,15]]},"location":"Linz, Austria","end":{"date-parts":[[2015,7,17]]}},"container-title":["2015 European Control Conference (ECC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7317886\/7330515\/07330941.pdf?arnumber=7330941","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T00:14:17Z","timestamp":1498263257000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7330941\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7]]},"references-count":27,"URL":"https:\/\/doi.org\/10.1109\/ecc.2015.7330941","relation":{},"subject":[],"published":{"date-parts":[[2015,7]]}}}