{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T06:17:10Z","timestamp":1725689830809},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642308840"},{"type":"electronic","value":"9783642308857"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30885-7_5","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T04:50:45Z","timestamp":1340772645000},"page":"65-78","source":"Crossref","is-referenced-by-count":1,"title":["Continuous ASM, and a Pacemaker Sensing Fragment"],"prefix":"10.1007","author":[{"given":"Richard","family":"Banach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wen","family":"Su","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaofeng","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1111\/j.1540-8159.1989.tb02696.x","volume":"12","author":"A. Aubert","year":"1989","unstructured":"Aubert, A., Goldreyer, B., Wyman, M., Jaquemlyn, E., Ector, H., de Geest, H.: Filter Characteristics of the Atrial Sensing Circuit of a Rate Responsive Pacemaker. To See or Not to See. PACE\u00a012, 525\u2013536 (1989)","journal-title":"PACE"},{"key":"5_CR4","unstructured":"Banach, R.: Model Based Refinement and the Design of Retrenchments. Available from [18]"},{"key":"5_CR5","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.jlap.2007.11.001","volume":"75","author":"R. Banach","year":"2008","unstructured":"Banach, R., Jeske, C., Poppleton, M.: Composition Mechanisms for Retrenchment. J. Log. Alg. Prog.\u00a075, 209\u2013229 (2008)","journal-title":"J. Log. Alg. Prog."},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/j.scico.2007.04.002","volume":"67","author":"R. Banach","year":"2007","unstructured":"Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Engineering and Theoretical Underpinnings of Retrenchment. Sci. Comp. Prog.\u00a067, 301\u2013329 (2007)","journal-title":"Sci. Comp. Prog."},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Barold, S., Stroobandt, R., Sinnaeve, A.: Cardiac Pacemakers and Resynchronization Step by Step: An Illustrated Guide. Wiley-Blackwell (2010)","DOI":"10.1002\/9781444323214"},{"key":"5_CR8","first-page":"237","volume":"15","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E.: The ASM Refinement Method. FACJ\u00a015, 237\u2013257 (2003)","journal-title":"FACJ"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract State Machines. A Method for High Level System Design and Analysis. Springer (2003)","DOI":"10.1007\/978-3-642-18216-7"},{"key":"5_CR10","unstructured":"Boston Scientific: PACEMAKER System Specification (2007), \n                    \n                      http:\/\/www.cas.mcmaster.ca\/sqrl\/_SQRLDocuments\/PACEMAKER.pdf"},{"key":"5_CR11","unstructured":"Ellenbogen, K., Wood, M.: Cardiac Pacing and ICDs, 5th edn. Wiley-Blackwell (2008)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-642-05089-3_44","volume-title":"FM 2009: Formal Methods","author":"A.O. Gomes","year":"2009","unstructured":"Gomes, A.O., Oliveira, M.V.M.: Formal Specification of a Cardiac Pacing System. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 692\u2013707. Springer, Heidelberg (2009)"},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1109\/MC.2006.145","volume":"39","author":"C. Jones","year":"2006","unstructured":"Jones, C., O\u2019Hearne, P., Woodcock, J.: Verified Software: A Grand Challenge. IEEE Computer\u00a039, 93\u201395 (2006)","journal-title":"IEEE Computer"},{"key":"5_CR14","unstructured":"Karlsruhe Interactive Verifier, \n                    \n                      http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/swt\/se\/kiv\/"},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1111\/j.1540-8159.1979.tb05171.x","volume":"2","author":"M. Keinert","year":"1979","unstructured":"Keinert, M., Elmqvist, H., Strandberg, H.: Spectral Properties of Atrial and Ventricular Endocardial Signals. PACE\u00a02, 11\u201319 (1979)","journal-title":"PACE"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-68237-0_14","volume-title":"FM 2008: Formal Methods","author":"H.D. Macedo","year":"2008","unstructured":"Macedo, H.D., Larsen, P.G., Fitzgerald, J.: Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 181\u2013197. Springer, Heidelberg (2008)"},{"key":"5_CR17","unstructured":"M\u00e9ry, D., Singh, N.: Functional Behavior of a Cardiac Pacing System. Tech. rep., LORIA, Universit\u00e9 Henri Poincar\u00e9 - Nancy I (2011), \n                    \n                      http:\/\/www.loria.fr\/~singhnne\/Home_files\/downloads\/ijdecs2010.pdf\n                    \n                    \n                  , Int. J. Discrete Event Control Systems"},{"key":"5_CR18","unstructured":"Retrenchment Homepage, \n                    \n                      http:\/\/www.cs.man.ac.uk\/retrenchment"},{"key":"5_CR19","first-page":"952","volume":"7","author":"G. Schellhorn","year":"2001","unstructured":"Schellhorn, G.: Verification of ASM Refinements Using Generalized Forward Simulation. JUCS\u00a07, 952\u2013979 (2001)","journal-title":"JUCS"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1016\/j.tcs.2004.11.013","volume":"336","author":"G. Schellhorn","year":"2005","unstructured":"Schellhorn, G.: ASM Refinement and Generalizations of Forward Simulation in Data Refinement: A Comparison. Theor. Comp. Sci.\u00a0336, 403\u2013435 (2005)","journal-title":"Theor. Comp. Sci."},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/j.eupc.2004.12.004","volume":"7","author":"A. Schuchert","year":"2005","unstructured":"Schuchert, A., Aydin, A., Israel, C., Gaby, G., Paul, V.: Arial Pacing and Sensing Characteristics in Heart Failure Patients Undergoing Cardiac Resynchronization Therapy. Europace\u00a07, 165\u2013169 (2005)","journal-title":"Europace"},{"key":"5_CR22","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1085\/jgp.16.3.423","volume":"16","author":"F. Wilson","year":"1933","unstructured":"Wilson, F., Macleod, A., Barker, P.: The Distribution of the Action Currents Produced by Heart Muscle and Other Excitable Tissues Immersed in Extensive Conducting Media. J. Gen. Physiol.\u00a016, 423\u2013456 (1933)","journal-title":"J. Gen. Physiol."},{"key":"5_CR23","series-title":"University of Michigan Studies. Scientific Series","volume-title":"The Distribution of the Currents of Action and of Injury Displayed by Heart Muscle and Other Excitable Tissues","author":"F. Wilson","year":"1933","unstructured":"Wilson, F., Macleod, A., Barker, P.: The Distribution of the Currents of Action and of Injury Displayed by Heart Muscle and Other Excitable Tissues. University of Michigan Studies. Scientific Series, vol.\u00a010. University of Michigan Press, Ann Arbor (1933); Reprinted in: Lepeschkin, Johnston (eds.) Selected Papers of Wilson, F.N., Edwards, J.W.: Ann Arbor (1954)"},{"key":"5_CR24","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1109\/MC.2006.340","volume":"39","author":"J. Woodcock","year":"2006","unstructured":"Woodcock, J.: First Steps in the The Verified Software Grand Challenge. IEEE Computer\u00a039, 57\u201364 (2006)","journal-title":"IEEE Computer"},{"key":"5_CR25","first-page":"661","volume":"13","author":"J. Woodcock","year":"2007","unstructured":"Woodcock, J., Banach, R.: The Verification Grand Challenge. JUCS\u00a013, 661\u2013668 (2007)","journal-title":"JUCS"},{"key":"5_CR26","unstructured":"Woodcock, J., Davies, J.: Using Z, Specification, Refinement and Proof. Prentice Hall (1996)"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30885-7_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:33:18Z","timestamp":1620113598000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30885-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642308840","9783642308857"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30885-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}