{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T23:26:27Z","timestamp":1725578787669},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642198281"},{"type":"electronic","value":"9783642198298"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19829-8_14","type":"book-chapter","created":{"date-parts":[[2011,3,16]],"date-time":"2011-03-16T14:20:41Z","timestamp":1300285241000},"page":"210-225","source":"Crossref","is-referenced-by-count":2,"title":["Formal Development of a Cardiac Pacemaker: From Specification to Code"],"prefix":"10.1007","author":[{"given":"Artur O.","family":"Gomes","sequence":"first","affiliation":[]},{"given":"Marcel V. M.","family":"Oliveira","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Software Quality Research Laboratory SQRL (2008), http:\/\/www.cas.mcmaster.ca\/sqrl\/"},{"key":"14_CR2","first-page":"363","volume-title":"SEFM 2005: Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods","author":"G. Carter","year":"2005","unstructured":"Carter, G., Monahan, R., Morris, J.M.: Software Refinement With Perfect Developer. In: SEFM 2005: Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, Washington, DC, USA, pp. 363\u2013373. IEEE Computer Society, Los Alamitos (2005)"},{"issue":"3","key":"14_CR3","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s001650050016","volume":"10","author":"A. Cavalcanti","year":"1998","unstructured":"Cavalcanti, A., Woodcock, J.: ZRC - A Refinement Calculus for Z. Formal Aspects of Computing\u00a010(3), 267\u2013289 (1998)","journal-title":"Formal Aspects of Computing"},{"key":"14_CR4","unstructured":"Celoxica. Handel-C language reference manual, v3.0 (2002)"},{"key":"14_CR5","unstructured":"Boston\u00a0Scientific Corporation. ALTRUA Pacemaker System Guide (2008)"},{"key":"14_CR6","unstructured":"de Oliveira, M.V.M.: Formal Derivation of State-Rich Reactive Programs Using Circus PhD thesis, Department of Computer Science, University of York (2005) YCST-2006\/02"},{"key":"14_CR7","unstructured":"Ellenbogen, K.A., Wood, M.A.: Cardiac Pacemakers and ICDs. Wiley-Blackwell (2005)"},{"key":"14_CR8","unstructured":"Gomes, A.O., de Oliveira, M.V.M.: Pacemaker Specification in Z Using ProofPower-Z"},{"key":"14_CR9","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., de 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":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-540-87603-8_37","volume-title":"Abstract State Machines, B and Z","author":"A.C. Gurgel","year":"2008","unstructured":"Gurgel, A.C., Castro, C.G., de Oliveira, M.V.M.: Tool Support for the Circus Refinement Calculus. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, p. 349. Springer, Heidelberg (2008)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Hoare, T.: The Verifying Compiler: A Grand Challenge for Computing Research. Journal of the ACM\u00a050 (2003)","DOI":"10.1145\/602382.602403"},{"key":"14_CR12","unstructured":"Hoare, T., Leavens, G.T., Misra, J., Shankar, N.: The Verified Software Initiative: A Manifesto (2007)"},{"key":"14_CR13","unstructured":"Software Quality\u00a0Research Laboratory. Pacemaker System Specification (2007), http:\/\/sqrl.mcmaster.ca\/_SQRLDocuments\/PACEMAKER.pdf"},{"key":"14_CR14","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.S.: Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM. In: Cu\u00e9llar, J., Maibaum, T.S.E., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 181\u2013197. Springer, Heidelberg (2008)"},{"key":"14_CR15","unstructured":"M\u00e9ry, D., Singh, N.K.: Pacemaker\u2019s Functional Behaviors in Event-B. Technical Report Version 2, Universit Henri Poincar Nancy 1 (2009)"},{"key":"14_CR16","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1109\/SEFM.2008.9","volume-title":"SEFM 2008: Proceedings of the 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods","author":"M.V.M. Oliveira","year":"2008","unstructured":"Oliveira, M.V.M., Gurgel, A.C., Castro, C.G.: CRefine: Support for the Circus Refinement Calculus. In: SEFM 2008: Proceedings of the 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods, Washington, DC, USA, 2008, pp. 281\u2013290. IEEE Computer Society, Los Alamitos (2008)"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying Theories in ProofPower-Z. Formal Aspects of Computing (2007)","DOI":"10.1007\/s00165-007-0044-5"},{"key":"14_CR18","first-page":"75","volume-title":"ISSS 2001: Proceedings of the 14th International Symposium on Systems Synthesis","author":"P.R. Panda","year":"2001","unstructured":"Panda, P.R.: SystemC: A Modeling Platform Supporting Multiple Design Abstractions. In: ISSS 2001: Proceedings of the 14th International Symposium on Systems Synthesis, pp. 75\u201380. ACM, New York (2001)"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-540-73210-5_25","volume-title":"Integrated Formal Methods","author":"D. Plagge","year":"2007","unstructured":"Plagge, D., Leuschel, M.: Validating Z Specifications using the ProB Animator and Model Checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 480\u2013500. Springer, Heidelberg (2007)"},{"key":"14_CR20","volume-title":"Concurrent and Real Time Systems: The CSP Approach","author":"S. Schneider","year":"1999","unstructured":"Schneider, S.: Concurrent and Real Time Systems: The CSP Approach. John Wiley & Sons, Inc., New York (1999)"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Sherif, A.: A Framework for Specification and Validation of Real-Time Systems using Circus Actions. PhD thesis, Center of Informatics - Federal University of Pernambuco, Brazil (2006)","DOI":"10.1007\/978-3-540-31862-0_34"},{"key":"14_CR22","volume-title":"Cardiac Pacemakers Step by Step \u2013 An Illustrated Guide","author":"R. Stroobandt","year":"2003","unstructured":"Stroobandt, R., Barold, A.F.S.S.: Cardiac Pacemakers Step by Step \u2013 An Illustrated Guide. Blackwell Publishing Ltd, Malden (2003)"},{"key":"14_CR23","first-page":"307","volume-title":"ISoLA. Communications in Computer and Information Science","author":"J. Sun","year":"2008","unstructured":"Sun, J., Liu, Y., Dong, J.S.: Model Checking CSP Revisited: Introducing a Process Analysis Toolkit. In: Margaria, T., Steffen, B. (eds.) ISoLA. Communications in Computer and Information Science, vol.\u00a017, pp. 307\u2013322. Springer, Heidelberg (2008)"},{"key":"14_CR24","volume-title":"Fourth IEEE International Conference on Secure Software Integration and Reliability Improvement","author":"L.A. Tuan","year":"2010","unstructured":"Tuan, L.A., Zheng, M.C., Tho, Q.T.: Modeling and Verification of Safety Critical Systems: A Case Study on Pacemaker. In: Fourth IEEE International Conference on Secure Software Integration and Reliability Improvement. IEEE Press, Los Alamitos (2010)"},{"key":"14_CR25","volume-title":"Using Z\u2013Specification, Refinement, and Proof","author":"J.C.P. Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z\u2013Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19829-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,20]],"date-time":"2021-11-20T11:12:28Z","timestamp":1637406748000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19829-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198281","9783642198298"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19829-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}