{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T10:11:51Z","timestamp":1649153511538},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2011,9,29]],"date-time":"2011-09-29T00:00:00Z","timestamp":1317254400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2011,12]]},"DOI":"10.1007\/s11334-011-0165-0","type":"journal-article","created":{"date-parts":[[2011,9,28]],"date-time":"2011-09-28T11:45:06Z","timestamp":1317210306000},"page":"227-235","source":"Crossref","is-referenced-by-count":1,"title":["A generic framework: from modeling to code"],"prefix":"10.1007","volume":"7","author":[{"given":"Dominique","family":"M\u00e9ry","sequence":"first","affiliation":[]},{"given":"Neeraj Kumar","family":"Singh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,9,29]]},"reference":[{"key":"165_CR1","doi-asserted-by":"crossref","unstructured":"Abrial J-R (1996) The B book\u2014assigning programs to meanings. Cambridge University Press","DOI":"10.1017\/CBO9780511624162"},{"key":"165_CR2","doi-asserted-by":"crossref","unstructured":"Abrial J-R (2010) Modeling in Event-B: system and software engineering","DOI":"10.1017\/CBO9781139195881"},{"issue":"7","key":"165_CR3","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1109\/TSE.2004.34","volume":"30","author":"L Apvrille","year":"2004","unstructured":"Apvrille L, Courtiat J-P, Lohr C, de Saqui-Sannes P (2004) Turtle: a real-time UML profile supported by a formal validation toolkit. IEEE Trans Softw Eng 30(7): 473\u2013487","journal-title":"IEEE Trans Softw Eng"},{"key":"165_CR4","doi-asserted-by":"crossref","unstructured":"Barold SS, Stroobandt RX, Sinnaeve AF (2004) Cardiac pacemakers step by step. Futura Publishing. ISBN:1-4051-1647-1","DOI":"10.1002\/9780470750728"},{"key":"165_CR5","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner D, Henson MC (eds) (2007) Logics of specification languages. EATCS textbook in computer science. Springer, Berlin","DOI":"10.1007\/978-3-540-74107-7"},{"key":"165_CR6","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner D, Jones CB (eds) (1978) The Vienna development method: the meta-language. Springer, London","DOI":"10.1007\/3-540-08766-4"},{"key":"165_CR7","unstructured":"Boston Scientific (2007) Boston Scientific: pacemaker system specification. Technical report"},{"key":"165_CR8","unstructured":"Cansell D, M\u00e9ry D (2007) The event-B modelling method: concepts and case studies. Springer, Berlin, pp 33\u2013140"},{"key":"165_CR9","unstructured":"Cansell D, M\u00e9ry D, Rehm J (2006) Formal specification and development in B. In: Time constraint patterns for Event B development. LNCS. Springer, pp 140\u2013154"},{"key":"165_CR10","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press. ISBN:978-0262032704"},{"key":"165_CR11","unstructured":"EB2ALL (2011) Automatic code generation from Event-B to many programming languages. http:\/\/eb2all.loria.fr\/"},{"key":"165_CR12","doi-asserted-by":"crossref","unstructured":"Faugere M, Bourbeau T, de Simone R, Gerard S (2007) Marte: also an uml profile for modeling AADL applications. Eng Complex Comput Syst IEEE 0:359\u2013364","DOI":"10.1109\/ICECCS.2007.29"},{"key":"165_CR13","unstructured":"Georg G, Bieman J, France RB (2001) Using alloy and UML\/OCL to specify run-time configuration management: a case study. In: Practical UML-based rigorous development methods\u2014countering or integrating the eXtremists, pp 128\u2013141"},{"key":"165_CR14","doi-asserted-by":"crossref","unstructured":"Hesselson A (2003) Simplified interpretations of pacemaker ECGs. Blackwell. ISBN:9781405103725","DOI":"10.1002\/9780470695982"},{"issue":"2","key":"165_CR15","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson D (2002) Alloy: a lightweight object modelling notation. ACM Trans Softw Eng Methodol 11(2): 256\u2013290","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"165_CR16","doi-asserted-by":"crossref","unstructured":"Leuschel M, Butler M (2003) ProB: a model checker for B. LNCS, Springer, pp 855\u2013874","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"165_CR17","unstructured":"Love CJ (2006) Cardiac pacemakers and defibrillators. Landes Bioscience Publishers. ISBN:1570596913"},{"key":"165_CR18","unstructured":"Malmivuo J (1995) Bioelectromagnetism. Oxford University Press. ISBN:0-19-505823-2"},{"key":"165_CR19","unstructured":"M\u00e9ry D, Singh NK (2010) EB2C: a tool for Event-B to C conversion support, poster and tool demo submission and published in a CNR Technical Report in SEFM"},{"key":"165_CR20","unstructured":"M\u00e9ry D, Singh NK (2011) Functional behavior of a cardiac pacing system. Int J Discrete Event Control Syst 1(2):129\u2013149"},{"key":"165_CR21","unstructured":"NITRD (2009) High confidence software and systems coordinating group, high-confidence medical devices: cyber-physical systems for 21st century health care. Technical report, NITRD. http:\/\/www.nitrd.gov\/About\/MedDevice-FINAL1-web.pdf"},{"key":"165_CR22","unstructured":"Overture Tool Box (2011) Overture: formal modelling in VDM. http:\/\/www.overturetool.org\/"},{"key":"165_CR23","unstructured":"ProB The ProB animator and model checker for the B method. http:\/\/www.stups.uni-duesseldorf.de\/ProB\/overview.php\/"},{"key":"165_CR24","unstructured":"Project RODIN (2004\u20132011) Rigorous open development environment for complex systems. http:\/\/rodin-b-sharp.sourceforge.net\/"},{"key":"165_CR25","unstructured":"Rumbaugh J, Jacobson I, Booch G (eds) (1999) The Unified Modeling Language reference manual. Addison-Wesley Longman Ltd., Essex"},{"key":"165_CR26","unstructured":"Smith JE, Kokar MK, Baclawski K (2001) Formal verification of UML diagrams: a first step towards code generation. In: Practical UML-based rigorous development methods\u2014countering or integrating the eXtremists, pp 224\u2013240"},{"key":"165_CR27","unstructured":"Snook C, Butler M (2004) U2B\u2014a tool for translating UML-B models into B"},{"key":"165_CR28","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C Snook","year":"2006","unstructured":"Snook C, Butler M (2006) UML-B: formal modeling and design aided by UML. ACM Trans Softw Eng Methodol 15: 92\u2013122","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"165_CR29","unstructured":"Vaziri M, Jackson D (2000) Some shortcomings of OCL, the object constraint language of UML. In: Proceedings of the technology of object-oriented languages and systems, TOOLS \u201900. IEEE Computer Society"},{"key":"165_CR30","unstructured":"Warmer J, Kleppe A (2003) The object constraint language: getting your models ready for MDA, 2nd edn. Addison-Wesley Longman Publishing Co., Boston"},{"key":"165_CR31","doi-asserted-by":"crossref","unstructured":"Members Writing Committee, Epstein AE, DiMarco JP, Ellenbogen KA, Estes III, Mark NA, Freedman RA, Gettes LS, Gillinov AM, Gregoratos G, Hammill SC, Hayes DL, Hlatky MA, Newby LK, Page RL, Schoenfeld MH, Silka MJ, Stevenson LW, Sweeney MO (2008) ACC\/AHA\/HRS 2008 guidelines for device-based therapy of cardiac rhythm abnormalities, developed in collaboration with the American Association for Thoracic Surgery and Society of Thoracic Surgeons. Circulation 117(21)","DOI":"10.1161\/CIRCUALTIONAHA.108.189742"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-011-0165-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-011-0165-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-011-0165-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,16]],"date-time":"2019-06-16T17:15:00Z","timestamp":1560705300000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-011-0165-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9,29]]},"references-count":31,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["165"],"URL":"https:\/\/doi.org\/10.1007\/s11334-011-0165-0","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,9,29]]}}}