Article

Formal development of a cardiac pacemaker: from specification to code

Authors:

Artur O. Gomes,

Marcel V. M. OliveiraAuthors Info & Claims

SBMF'10: Proceedings of the 13th Brazilian conference on Formal methods: foundations and applications

Pages 210 - 225

Published: 08 November 2010 Publication History

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.

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)

Digital Library

[3]

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

[4]

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

[5]

Boston Scientific Corporation. ALTRUA Pacemaker System Guide (2008)

[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

[7]

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

[8]

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

[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)

Digital Library

[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)

Digital Library

[11]

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

Digital Library

[12]

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

[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)

Digital Library

[15]

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

[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)

Digital Library

[17]

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

[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)

Digital Library

[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)

Digital Library

[20]

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

Digital Library

[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)

[22]

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

[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)

[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)

Digital Library

[25]

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

Digital Library

Cited By

Madala KDo HAceituna DChaudron MCrnkovic IChechik MHarman M(2018)A combinatorial approach for exposing off-nominal behaviorsProceedings of the 40th International Conference on Software Engineering10.1145/3180155.3180204(910-920)Online publication date: 27-May-2018
https://dl.acm.org/doi/10.1145/3180155.3180204
Banach RZhu HSu WWu X(2014)A Continuous ASM Modelling Approach to Pacemaker SensingACM Transactions on Software Engineering and Methodology10.1145/261037524:1(1-40)Online publication date: 7-Oct-2014
https://dl.acm.org/doi/10.1145/2610375

Recommendations

Formal Specification of a Cardiac Pacing System
FM '09: Proceedings of the 2nd World Congress on Formal Methods

The International Grand Challenge project on Verified Software is a long-term research program involving people from all over the world and is aimed to stimulate the creation of new theories and tools to be applied on industrial-scale problems. One of ...
Formal semantics for the PACEMAKER system specification
HILT '14: Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology

This paper formally expresses the timing behavior of a cardiac pacemaker as defined in the PACEMAKER System Specification as understood by its principal author.

The PACEMAKER System Specification was publicly released by Boston Scientific to provide a ...
Formal semantics for the PACEMAKER system specification
HILT '14

This paper formally expresses the timing behavior of a cardiac pacemaker as defined in the PACEMAKER System Specification as understood by its principal author.

The PACEMAKER System Specification was publicly released by Boston Scientific to provide a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SBMF'10: Proceedings of the 13th Brazilian conference on Formal methods: foundations and applications

November 2010

290 pages

ISBN:9783642198281

Editors:
Jim Davies
Oxford University, Department of Computer Science, Oxford, UK
,
Leila Silva
Universidade Federal de Sergipe, Departamento de Ciência da Computação e Estatística, Aracaju, SE, Brazil
,
Adenilso Simao
Avenida Trabalhador São-Carlense, São Carlos, SP, Brazil

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 08 November 2010

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Madala KDo HAceituna DChaudron MCrnkovic IChechik MHarman M(2018)A combinatorial approach for exposing off-nominal behaviorsProceedings of the 40th International Conference on Software Engineering10.1145/3180155.3180204(910-920)Online publication date: 27-May-2018
https://dl.acm.org/doi/10.1145/3180155.3180204
Banach RZhu HSu WWu X(2014)A Continuous ASM Modelling Approach to Pacemaker SensingACM Transactions on Software Engineering and Methodology10.1145/261037524:1(1-40)Online publication date: 7-Oct-2014
https://dl.acm.org/doi/10.1145/2610375

View Options

View options

Media

Figures

Other

Tables

View Table of Contents