research-article

A Continuous ASM Modelling Approach to Pacemaker Sensing

Authors:

Richard Banach,

Xiaofeng WuAuthors Info & Claims

ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 24, Issue 1

Article No.: 2, Pages 1 - 40

https://doi.org/10.1145/2610375

Published: 07 October 2014 Publication History

Abstract

The cardiac pacemaker system, proposed as a problem topic in the Verification Grand Challenge, offers a range of difficulties to address for formal specification, development, and verification technologies. We focus on the sensing problem, the question of whether the heart has produced a spontaneous heartbeat or not. This question is plagued by uncertainties arising from the often unpredictable environment that a real pacemaker finds itself in. We develop a time domain tracking approach to this problem, as a complement to the usual frequency domain approach most frequently used. We develop our case study in the continuous ASM (Abstract State Machine) formalism, which is briefly summarised, through a series of refinement and retrenchment steps, each adding new levels of complexity to the model.

References

[1]

R. Alur, C. Courcoubetis, T. Henzinger, and P.-H. Ho. 1993. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Proceedings of the Workshop on Theory of Hybrid Systems. Lecture Notes in Computer Science, vol. 736, Springer, 209--229.

Digital Library

[2]

R. Alur and D. Dill. 1994. A theory of timed automata. Theoret. Comp. Sci. 126, 183--235.

Digital Library

[3]

A. Aubert, B. Goldreyer, M. Wyman, E. Jaquemlyn, H. Ector, and H. de Geest. 1989. Filter characteristics of the atrial sensing circuit of a rate responsive pacemaker. To see or not to see. PACE 12, 525--536.

[4]

R. Banach and C. Jeske. 2014. Retrenchment and refinement interworking: The tower theorems. Math. Struc. Comp. Sci, To appear. http://www.cs.man.ac.uk/&sim;banach/some.pubs/Retrench.Tower.pdf.

[5]

R. Banach, C. Jeske, and M. Poppleton. 2008. Composition mechanisms for retrenchment. J. Log. Alg. Prog. 75, 209--229.

[6]

R. Banach, M. Poppleton, C. Jeske, and S. Stepney. 2007. Engineering and theoretical underpinnings of retrenchment. Sci. Comp. Prog. 67, 301--329.

Digital Library

[7]

R. Banach, H. Zhu, W. Su, and X. Wu. 2014. Moded and continuous ASM. Submitted.

[8]

S. Barold, R. Stroobandt, and A. Sinnaeve. 2010. Cardiac Pacemakers and Resynchronization Step by Step: An Illustrated Guide. Wiley-Blackwell.

[9]

L. Barolli, M. Takizawa, and F. Hussain. 2011. Special issue on emerging trends in cyber-physical systems. J. Amb. Intel. Hum. Comp. 2, 249--250.

[10]

E. Börger. 2003. The ASM refinement method. Form. Aspects Comput. 15, 237--257.

Digital Library

[11]

E. Börger and R. F. Stärk. 2003. Abstract State Machines. A Method for High Level System Design and Analysis. Springer.

Digital Library

[12]

Boston Scientific. 2007. PACEMAKER system specification. http://www.cas.mcmaster.ca/sqrl/_SQRL Documents/PACEMAKER.pdf.

[13]

L. Britnell, R. Gorbachev, R. Jalil, et al. 2012. Field-effect tunneling transistor based on vertical graphene heterostructures. Science.

[14]

L. Carloni, R. Passerone, A. Pinto, and A. Sangiovanni-Vincentelli. 2006. Languages and tools for hybrid systems design. Found. Trends Elect. Des. Automat. 1, 1--193.

Digital Library

[15]

E. Clarke and P. Zuliani. 2011. Statistical model checking for cyber-physical systems. In Proceedings of ATVA-11, Lecture Notes in Computer Science, T. Bultan and P.-A. Hsiung (Eds.), vol. 6996, Springer, 1--12.

Digital Library

[16]

CPS. 2008. Report: Cyber-Physical Systems. http://iccps2012.cse.wustl.edu/_doc/CPS_Summit_Report.pdf.

[17]

J. Davoren. 2009. Epsilon-Tubes and Generalized Skorokhod Metrics for Hybrid Paths Spaces. In Proc. HSCC-09. Lecture Notes in Computer Science, vol. 5469, Springer, 135--149.

Digital Library

[18]

V. DeCaprio, P. Hurzeler, and S. Furman. 1977. A comparison of unipolar and bipolar electrograms for cardiac pacemaker sensing. Circulation 56, 750--755.

[19]

L. Doyen, T. Henzinger, and J.-F. Raskin. 2005. Automatic rectangular refinement of affine hybrid systems. In Proceedings of FORMATS-05. Lecture Notes in Computer Science, vol. 3829, Springer, 144--161.

Digital Library

[20]

K. Ellenbogen, B. Wilkoff, G. Kay, and C-P. Lau. 2006. Clinical Cardiac Pacing, Defibrillation and Resynchronization Therapy. Saunders.

[21]

K. Ellenbogen and M. Wood. 2008. Cardiac Pacing and ICDs. Wiley-Blackwell. 5th ed.

[22]

S. Furman, P. Hurzeler, and V. DeCaprio. 1977. Cardiac pacing and pacemakers III: Sensing the cardiac electrogram. Amer. Heart J. 93, 794--801.

[23]

A. Geim and K. Novoselov. 2007. The rise of graphene. Nature Mater. 6, 183--191.

[24]

R. Gilmore. 1981. Catastrophe Theory for Scientists and Engineers. Dover.

[25]

A. Girard, A. Julius, and G. Pappas. 2008. Approximate simulation relations for hybrid systems. Disc. Event Dyn. Syst. 18 (2008), 163--179.

Digital Library

[26]

B. Goldman, E. Noble, J. Heller, and D. Covvey. 1974. The pacemaker challenge. Can. Med. Ass. J. 10, 28--31.

[27]

A. Gomes and M. Oliveira. 2009. Formal specification of a cardiac pacing system. In Proceedings of FM-09. Lecture Notes in Computer Science, vol. 5850, Springer, 692--707.

Digital Library

[28]

A. Gomes and M. Oliveira. 2010. Formal development of cardiac pacemaker: From specification to code. In Proceedings of SBMF-10. Lecture Notes in Computer Science, vol. 6527, Springer, 210--225.

Digital Library

[29]

J. He. 1994. From CSP to hybrid systems. In A Classical Mind, Essays in Honour of C.A.R. Hoare, Roscoe (Ed.), Prentice-Hall, 171--189.

Digital Library

[30]

T. Henzinger. 1996. The theory of hybrid automata. In Proceedings of IEEE LICS-96. IEEE, 278--292. Also http://mtc.epfl.ch/&sim;tah/Publications/the_theory_of_hybrid_automata.pdf.

Digital Library

[31]

C. B. Jones, P. O'Hearne, and J. Woodcock. 2006. Verified software: A grand challenge. IEEE Comput. 39, 93--95.

Digital Library

[32]

M. Keinert, H. Elmqvist, and H. Strandberg. 1979. Spectral properties of atrial and ventricular endocardial signals. PACE 2, 11--19.

[33]

KIV. Karlsruhe Interactive Verifier. http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/kiv/.

[34]

F. Kusumoto and N. Goldschlager. 2007. Cardiac Pacing for the Clinician. Springer.

[35]

E. Lee. 2006. Cyber-physical systems—Are computing foundations adequate. In Proceedings of the NSF Workshop on Cyber-Physical Systems: Research Motivation, Techniques and Roadmap.

[36]

E. Lee. 2008. Cyber-physical systems: Design challenges. In Proceedings of ISORC-08. Invited Paper. http://chess.eecs.berkeley.edu/pubs/427.html.

Digital Library

[37]

E. Lee and S. Sesha. 2013. Introduction to Embedded Systems - A Cyber-Physical Systems Approach. Lulu.com.

[38]

H. Macedo, P. Larsen, and J. Fitzgerald. 2008. Incremental development of a distributed real-time model of a cardiac pacing system using VDM. In Proceedings of FM-08. Lecture Notes in Computer Science, vol. 5014, Springer, 181--197.

Digital Library

[39]

D. Méry and N. Singh. 2009. Pacemaker's functional behaviors in event-B. Tech. Rep. INRIA-00419973:2. LORIA, Université Henri Poincaré - Nancy I. http://hal.inria.fr/inria-00419973/PDF/Pacemaker.pdf.

[40]

D. Méry and N. Singh. 2010. Technical report on formal development of two-electrode cardiac pacing system. Tech. Rep. INRIA-00465061:2. LORIA, Université Henri Poincaré - Nancy I. http://hal.inria.fr/inria-00465061/PDF/Report_2electrode.pdf.

[41]

D. Méry and N. Singh. 2011. Functional behavior of a cardiac pacing system. Tech. Rep. LORIA, Université Henri Poincaré - Nancy I. http://www.loria.fr/&sim;singhnne/Home_files/downloads/ijdecs2010.pdf, Int. J. Disc. Event Control Syst.

[42]

National Science and Technology Council. 2011. Trustworthy cyberspace: Strategic plan for the federal cybersecurity research and development program. http://www.whitehouse.gov/sites/default/files/microsites/ostp/fed_cybersecurity_rd_strategic_plan_2011.pdf.

[43]

A. Platzer. 2010. Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer.

Digital Library

[44]

J.-D. Quesel, M. Franzle, and W. Damm. 2011. Crossing the bridge between similar games. In Proceedings of the FORMATS-11. Lecture Notes in Computer Science, vol. 6919, Springer, 160--176.

Digital Library

[45]

RET. Retrenchment Homepage. http://www.cs.man.ac.uk/retrenchment.

[46]

P. Saunders. 1980. An Introduction to Catastrophe Theory. Cambridge University Press.

[47]

G. Schellhorn. 2001. Verification of ASM refinements using generalized forward simulation. J. Univ. Comput. Sci. 7, 952--979.

[48]

G. Schellhorn. 2005. ASM refinement and generalizations of forward simulation in data refinement: A comparison. Theoret. Comput. Sci. 336, 403--435.

Digital Library

[49]

A. Schuchert, A. Aydin, C. Israel, G. Gaby, and V. Paul. 2005. Arial pacing and sensing characteristics in heart failure patients undergoing cardiac resynchronization therapy. Europace 7, 165--169.

[50]

T. Stauner. 2002. Discrete-time refinement of hybrid automata. In Proceedings of HSCC-02. Lecture Notes in Computer Science, vol. 2289, Springer, 144--161.

Digital Library

[51]

M. Stehr, M. Kim, and C. Talcott. 2010. Toward distributed declarative control of networked cyber-physical systems. In Proc. UIC-10. Lecture Notes in Computer Science, vol. 6406. Z. Yu, R. Liscano, G. Chen, D. Zhang, and X. Zhou (Eds.), Springer, 397--413.

Digital Library

[52]

J. Sztipanovits. 2011. Model integration and cyber physical systems: A semantics perspective. In Proceedings of FM-11. Lecture Notes in Computer Science, vol. 6664, M. Butler and W. Schulte (Eds.). Springer, p. 1, http://sites.lero.ie/download.aspx&quest;f=Sztipanovits-Keynote.pdf. Invited talk, FM 2011, Limerick, Ireland.

Digital Library

[53]

P. Tabuada. 2009. Verification and Control of Hybrid Systems: A Symbolic Approach. Springer.

Digital Library

[54]

J. White, S. Clarke, C. Groba, B. Dougherty, C. Thompson, and D. Schmidt. 2010. R&D challenges and solutions for mobile cyber-physical applications and supporting internet services. J. Internet Serv. Appl. 1, 45--56.

[55]

J. Willems. 2007. Open dynamical systems: Their aims and their origins. Ruberti Lecture, Rome. http://homes. esat.kuleuven.be/&sim;jwillems/Lectures/2007/Rubertilecture.pdf.

[56]

F. Wilson, A. Macleod, and P. Barker. 1933a. The distribution of the action currents produced by heart muscle and other excitable tissues immersed in extensive conducting media. J. Gen. Physiol. 16, 423--456.

[57]

F. Wilson, A. Macleod, and P. Barker. 1933b. 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. 10, Ann Arbor: University of Michigan Press. (Reprinted in: Lepeschkin and Johnston (eds.), Selected Papers of Frank N. Wilson. Ann Arbor, J.W. Edwards (1954).)

[58]

J. Woodcock. 2006. First steps in the the verified software grand challenge. IEEE Computer 39, 57--64.

Digital Library

[59]

J. Woodcock and R. Banach. 2007. The verification grand challenge. JUCS 13, 661--668.

[60]

L. Zhang and J. He. 2011. A formal framework for aspect-oriented specification of cyber physical systems. In Proceedings of ICHIT-11. Communications in Computer and Information Science, vol. 206, G. Lee, D. Howard, and V. Slezak (Eds.), Springer, 391--398.

[61]

L. Zühlke and L. Ollinger. 2012. Agile automaton sysytems based on cyber-physical systems and service oriented architectures. In Proceedings ICAR-11. Lecture Notes in Electrical Engineering, vol. 122, G. Lee (Ed.), Springer, 567--574.

Cited By

Buga AMashkoor ANemeş SSchewe KSongprasop P(2018)An Event-B-based approach to hybrid systems engineering and its application to a hemodialysis machine case studyComputer Languages, Systems & Structures10.1016/j.cl.2018.07.00454(297-315)Online publication date: Dec-2018
https://doi.org/10.1016/j.cl.2018.07.004
Schewe KTec LWang Q(2018)Capturing Membrane Computing by ASMsAbstract State Machines, Alloy, B, TLA, VDM, and Z10.1007/978-3-319-91271-4_27(380-385)Online publication date: 8-May-2018
https://doi.org/10.1007/978-3-319-91271-4_27
Mashkoor AKossak FEgyed A(2018)Evaluating the suitability of state‐based formal methods for industrial deploymentSoftware: Practice and Experience10.1002/spe.263448:12(2350-2379)Online publication date: 13-Sep-2018
https://doi.org/10.1002/spe.2634
Show More Cited By

Index Terms

A Continuous ASM Modelling Approach to Pacemaker Sensing
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program specifications

Recommendations

Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
Abstract
A very simple model for train stopping is used as a vehicle for investigating how the development of a control system, initially designed in the continuous domain and subsequently discretized, can be captured within a formal development process ...
Researchers Fight to Keep Implanted Medical Devices Safe from Hackers

Implantable medical devices have become increasingly popular, and a growing number are equipped with wireless communications technology to increase their usefulness. However, this could make the devices susceptible to hackers.
Continuous ASM, and a pacemaker sensing fragment
ABZ'12: Proceedings of the Third international conference on Abstract State Machines, Alloy, B, VDM, and Z

The ASM framework is extended to include continuously varying quantities as well as conventional discretely changing ones. This opens the door to the more faithful modeling of many scenarios where digital systems have to interact with the continuously ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Software Engineering and Methodology

ACM Transactions on Software Engineering and Methodology Volume 24, Issue 1

September 2014

226 pages

ISSN:1049-331X

EISSN:1557-7392

DOI:10.1145/2676679

Editor:
David S. Rosenblum
National University of Singapore, Singapore

Issue’s Table of Contents

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 October 2014

Accepted: 01 April 2014

Revised: 01 January 2014

Received: 01 September 2013

Published in TOSEM Volume 24, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

National Natural Science Foundation of China
Ministry of Science and Technology of the People's Republic of China
Shanghai Knowledge Service Platform Project (No. ZF1213)
East China Normal University
Shanghai Minhang Talent Project

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
286
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)2

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Buga AMashkoor ANemeş SSchewe KSongprasop P(2018)An Event-B-based approach to hybrid systems engineering and its application to a hemodialysis machine case studyComputer Languages, Systems & Structures10.1016/j.cl.2018.07.00454(297-315)Online publication date: Dec-2018
https://doi.org/10.1016/j.cl.2018.07.004
Schewe KTec LWang Q(2018)Capturing Membrane Computing by ASMsAbstract State Machines, Alloy, B, TLA, VDM, and Z10.1007/978-3-319-91271-4_27(380-385)Online publication date: 8-May-2018
https://doi.org/10.1007/978-3-319-91271-4_27
Mashkoor AKossak FEgyed A(2018)Evaluating the suitability of state‐based formal methods for industrial deploymentSoftware: Practice and Experience10.1002/spe.263448:12(2350-2379)Online publication date: 13-Sep-2018
https://doi.org/10.1002/spe.2634
Bonfanti SGargantini AMashkoor A(2018)A systematic literature review of the use of formal methods in medical software systemsJournal of Software: Evolution and Process10.1002/smr.194330:5(e1943)Online publication date: 27-Feb-2018
https://doi.org/10.1002/smr.1943
Kossak FMashkoor A(2016)How to Select the Suitable Formal Method forźan Industrial ApplicationProceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 967510.1007/978-3-319-33600-8_13(213-228)Online publication date: 23-May-2016
https://dl.acm.org/doi/10.1007/978-3-319-33600-8_13
Banach RZhu HSu WWu X(2014)ASM, controller synthesis, and complete refinementScience of Computer Programming10.1016/j.scico.2014.04.01394:P2(109-129)Online publication date: 1-Oct-2014
https://dl.acm.org/doi/10.1016/j.scico.2014.04.013

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents