{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T06:42:03Z","timestamp":1729665723965,"version":"3.28.0"},"reference-count":29,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1109\/iccps.2014.6843718","type":"proceedings-article","created":{"date-parts":[[2014,7,28]],"date-time":"2014-07-28T17:09:21Z","timestamp":1406567361000},"page":"139-150","source":"Crossref","is-referenced-by-count":10,"title":["Linking abstract analysis to concrete design: A hierarchical approach to verify medical CPS safety"],"prefix":"10.1109","author":[{"given":"Anitha","family":"Murugesan","sequence":"first","affiliation":[]},{"given":"Oleg","family":"Sokolsky","sequence":"additional","affiliation":[]},{"given":"Sanjai","family":"Rayadurgam","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Whalen","sequence":"additional","affiliation":[]},{"given":"Mats","family":"Heimdahl","sequence":"additional","affiliation":[]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"year":"0","journal-title":"Simulink Design Verifier","key":"19"},{"doi-asserted-by":"publisher","key":"17","DOI":"10.1145\/1289927.1289949"},{"year":"0","key":"18"},{"year":"1968","author":"kamp","journal-title":"Tense logic and the theory of linear order","key":"15"},{"doi-asserted-by":"publisher","key":"16","DOI":"10.1145\/2038642.2038667"},{"key":"13","first-page":"957","article-title":"Discretization of timed automata","author":"go?llu?","year":"1994","journal-title":"Proceedings of the 33rd IEEE Conference on Decision and Control"},{"key":"14","first-page":"545","article-title":"What good are digital clocks?","volume":"623","author":"henzinger","year":"1992","journal-title":"Proceedings of the ICALEO 1992"},{"key":"11","doi-asserted-by":"crossref","first-page":"956","DOI":"10.1109\/TSE.2002.1041052","article-title":"The mo?bius framework and its implementation","volume":"28","author":"deavours","year":"2002","journal-title":"Software Engineering IEEE Transactions on"},{"key":"12","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","article-title":"DPLL(T): Fast decision procedures","volume":"3114","author":"ganzinger","year":"2004","journal-title":"Proceedings of the 16th International Conference on Computer Aided Verification CAV'04 (Boston Massachusetts)"},{"key":"21","article-title":"Circular compositional reasoning about liveness","author":"mcmillan","year":"1999","journal-title":"Technical Report 1999-02"},{"year":"0","key":"20"},{"doi-asserted-by":"publisher","key":"22","DOI":"10.1145\/2527269.2527272"},{"doi-asserted-by":"publisher","key":"23","DOI":"10.1109\/RTAS.2012.25"},{"key":"24","first-page":"1","article-title":"Model-driven safety analysis of closed-loop medical systems","author":"pajic","year":"2012","journal-title":"Industrial Informatics IEEE Transactions on"},{"doi-asserted-by":"publisher","key":"25","DOI":"10.1145\/2461328.2461368"},{"year":"2004","journal-title":"Architecture Analysis and Design Language","key":"26"},{"key":"27","first-page":"108","article-title":"Checking safety properties using induction and a sat-solver","volume":"1954","author":"sheeran","year":"2000","journal-title":"FMCAD"},{"key":"28","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/s10270-003-0039-5","article-title":"The OsMoSys approach to multi-formalism modeling of systems","volume":"3","author":"vittorini","year":"2004","journal-title":"Software and Systems Modeling"},{"doi-asserted-by":"publisher","key":"29","DOI":"10.2337\/dc07-1967"},{"key":"3","first-page":"200","article-title":"A tutorial on uppaal","author":"behrmann","year":"2004","journal-title":"Formal Methods for the Design of Real-Time Systems (Revised Lectures) Volume 3185 of LNCS"},{"doi-asserted-by":"publisher","key":"2","DOI":"10.1109\/MC.2003.1193228"},{"key":"10","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/3-540-45923-5_12","article-title":"AToM3: A tool for multi-formalism and meta-modelling","author":"de lara","year":"2002","journal-title":"Fundamental Approaches to Software Engineering"},{"year":"0","journal-title":"Infusion Pumps","key":"1"},{"doi-asserted-by":"publisher","key":"7","DOI":"10.1109\/RBME.2009.2036073"},{"key":"6","article-title":"A single-chip pulsoximeter design using the MSP430","author":"chan","year":"2005","journal-title":"Technical Report SLAA274"},{"key":"5","first-page":"527","article-title":"Readings in hardware\/software co-design","author":"buck","year":"2002","journal-title":"Ptolemy A Framework for Simulating and Prototyping Heterogeneous Systems"},{"year":"2003","author":"bequette","journal-title":"Process Control Modeling Design and Simulation","key":"4"},{"doi-asserted-by":"publisher","key":"9","DOI":"10.1109\/HCMDSS-MDPnP.2007.8"},{"key":"8","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","article-title":"Compositional verification of architectural models","volume":"7226","author":"cofer","year":"2012","journal-title":"Proc of 4th NASA Formal Methods Symposium (NFM)"}],"event":{"name":"2014 ACM\/IEEE International Conference on Cyber-Physical Systems (ICCPS)","start":{"date-parts":[[2014,4,14]]},"location":"Berlin, Germany","end":{"date-parts":[[2014,4,17]]}},"container-title":["2014 ACM\/IEEE International Conference on Cyber-Physical Systems (ICCPS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6834857\/6843703\/06843718.pdf?arnumber=6843718","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,14]],"date-time":"2020-10-14T11:38:54Z","timestamp":1602675534000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/6843718"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4]]},"references-count":29,"URL":"https:\/\/doi.org\/10.1109\/iccps.2014.6843718","relation":{},"subject":[],"published":{"date-parts":[[2014,4]]}}}