Abstract
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 varying physical world. Transitions in the extended framework are thus either moded (for discontinuous changing quantities), or pliant (for smoothly changing quantities). Refinement and retrenchment are defined in the extended context. The framework is used to develop a fragment of a simple system for the sensing problem for cardiac pacemakers, in the context of the pacemaker verification challenge.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
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 12, 525–536 (1989)
Banach, R.: Model Based Refinement and the Design of Retrenchments. Available from [18]
Banach, R., Jeske, C., Poppleton, M.: Composition Mechanisms for Retrenchment. J. Log. Alg. Prog. 75, 209–229 (2008)
Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Engineering and Theoretical Underpinnings of Retrenchment. Sci. Comp. Prog. 67, 301–329 (2007)
Barold, S., Stroobandt, R., Sinnaeve, A.: Cardiac Pacemakers and Resynchronization Step by Step: An Illustrated Guide. Wiley-Blackwell (2010)
Börger, E.: The ASM Refinement Method. FACJ 15, 237–257 (2003)
Börger, E., Stärk, R.: Abstract State Machines. A Method for High Level System Design and Analysis. Springer (2003)
Boston Scientific: PACEMAKER System Specification (2007), http://www.cas.mcmaster.ca/sqrl/_SQRLDocuments/PACEMAKER.pdf
Ellenbogen, K., Wood, M.: Cardiac Pacing and ICDs, 5th edn. Wiley-Blackwell (2008)
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. 5850, pp. 692–707. Springer, Heidelberg (2009)
Jones, C., O’Hearne, P., Woodcock, J.: Verified Software: A Grand Challenge. IEEE Computer 39, 93–95 (2006)
Karlsruhe Interactive Verifier, http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/kiv/
Keinert, M., Elmqvist, H., Strandberg, H.: Spectral Properties of Atrial and Ventricular Endocardial Signals. PACE 2, 11–19 (1979)
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. 5014, pp. 181–197. Springer, Heidelberg (2008)
Méry, D., Singh, N.: Functional Behavior of a Cardiac Pacing System. Tech. rep., LORIA, Université Henri Poincaré - Nancy I (2011), http://www.loria.fr/~singhnne/Home_files/downloads/ijdecs2010.pdf , Int. J. Discrete Event Control Systems
Retrenchment Homepage, http://www.cs.man.ac.uk/retrenchment
Schellhorn, G.: Verification of ASM Refinements Using Generalized Forward Simulation. JUCS 7, 952–979 (2001)
Schellhorn, G.: ASM Refinement and Generalizations of Forward Simulation in Data Refinement: A Comparison. Theor. Comp. Sci. 336, 403–435 (2005)
Schuchert, A., Aydin, A., Israel, C., Gaby, G., Paul, V.: Arial Pacing and Sensing Characteristics in Heart Failure Patients Undergoing Cardiac Resynchronization Therapy. Europace 7, 165–169 (2005)
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. 16, 423–456 (1933)
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. 10. University of Michigan Press, Ann Arbor (1933); Reprinted in: Lepeschkin, Johnston (eds.) Selected Papers of Wilson, F.N., Edwards, J.W.: Ann Arbor (1954)
Woodcock, J.: First Steps in the The Verified Software Grand Challenge. IEEE Computer 39, 57–64 (2006)
Woodcock, J., Banach, R.: The Verification Grand Challenge. JUCS 13, 661–668 (2007)
Woodcock, J., Davies, J.: Using Z, Specification, Refinement and Proof. Prentice Hall (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Banach, R., Zhu, H., Su, W., Wu, X. (2012). Continuous ASM, and a Pacemaker Sensing Fragment. In: Derrick, J., et al. Abstract State Machines, Alloy, B, VDM, and Z. ABZ 2012. Lecture Notes in Computer Science, vol 7316. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30885-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-30885-7_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30884-0
Online ISBN: 978-3-642-30885-7
eBook Packages: Computer ScienceComputer Science (R0)