Skip to main content
SpringerLink
Log in

Formal Development of a Cardiac Pacemaker: From Specification to Code

  • Conference paper
Formal Methods: Foundations and Applications (SBMF 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6527))

Included in the following conference series:

Abstract

This paper presents a formal development of a cardiac pacing system based on a Boston Scientific’s model, a pilot case study from the Grand Challenge in Software Verification. We present a summary of our Z model of the system, its translation into Perfect Developer, and the code generation and execution. Further practical result and analysis are also in the context of this paper.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Software Quality Research Laboratory SQRL (2008), http://www.cas.mcmaster.ca/sqrl/

  2. 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–373. IEEE Computer Society, Los Alamitos (2005)

    Google Scholar 

  3. Cavalcanti, A., Woodcock, J.: ZRC - A Refinement Calculus for Z. Formal Aspects of Computing 10(3), 267–289 (1998)

    Article  MATH  Google Scholar 

  4. Celoxica. Handel-C language reference manual, v3.0 (2002)

    Google Scholar 

  5. Boston Scientific Corporation. ALTRUA Pacemaker System Guide (2008)

    Google Scholar 

  6. 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

    Google Scholar 

  7. Ellenbogen, K.A., Wood, M.A.: Cardiac Pacemakers and ICDs. Wiley-Blackwell (2005)

    Google Scholar 

  8. Gomes, A.O., de Oliveira, M.V.M.: Pacemaker Specification in Z Using ProofPower-Z

    Google Scholar 

  9. 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. 5850, pp. 692–707. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  10. Gurgel, A.C., Castro, C.G., de Oliveira, M.V.M.: Tool Support for the Circus Refinement Calculus. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, p. 349. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Hoare, T.: The Verifying Compiler: A Grand Challenge for Computing Research. Journal of the ACM 50 (2003)

    Google Scholar 

  12. Hoare, T., Leavens, G.T., Misra, J., Shankar, N.: The Verified Software Initiative: A Manifesto (2007)

    Google Scholar 

  13. Software Quality Research Laboratory. Pacemaker System Specification (2007), http://sqrl.mcmaster.ca/_SQRLDocuments/PACEMAKER.pdf

  14. 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éllar, J., Maibaum, T.S.E., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 181–197. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  15. Méry, D., Singh, N.K.: Pacemaker’s Functional Behaviors in Event-B. Technical Report Version 2, Universit Henri Poincar Nancy 1 (2009)

    Google Scholar 

  16. 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–290. IEEE Computer Society, Los Alamitos (2008)

    Chapter  Google Scholar 

  17. Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying Theories in ProofPower-Z. Formal Aspects of Computing (2007)

    Google Scholar 

  18. 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–80. ACM, New York (2001)

    Google Scholar 

  19. Plagge, D., Leuschel, M.: Validating Z Specifications using the ProB Animator and Model Checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 480–500. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  20. Schneider, S.: Concurrent and Real Time Systems: The CSP Approach. John Wiley & Sons, Inc., New York (1999)

    Google Scholar 

  21. 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)

    Google Scholar 

  22. Stroobandt, R., Barold, A.F.S.S.: Cardiac Pacemakers Step by Step – An Illustrated Guide. Blackwell Publishing Ltd, Malden (2003)

    Google Scholar 

  23. 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. 17, pp. 307–322. Springer, Heidelberg (2008)

    Google Scholar 

  24. 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)

    Google Scholar 

  25. Woodcock, J.C.P., Davies, J.: Using Z–Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidade Federal do Rio Grande do Norte, Brazil

    Artur O. Gomes & Marcel V. M. Oliveira

Authors
  1. Artur O. Gomes
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marcel V. M. Oliveira
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Oxford University, OX1 3QD, Oxford, UK

    Jim Davies

  2. Departamento de Ciência da Computação e Estatística, Universidade Federal de Sergipe, CEP 49100-000, Aracaju, SE, Brazil

    Leila Silva

  3. Avenida Frabalhador, são-carlense, 400 Centro, 13566-590, São Carlos, SP, Brazil

    Adenilso Simao

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gomes, A.O., Oliveira, M.V.M. (2011). Formal Development of a Cardiac Pacemaker: From Specification to Code. In: Davies, J., Silva, L., Simao, A. (eds) Formal Methods: Foundations and Applications. SBMF 2010. Lecture Notes in Computer Science, vol 6527. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19829-8_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-19829-8_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-19828-1

  • Online ISBN: 978-3-642-19829-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation