Continuous ASM, and a Pacemaker Sensing Fragment

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{BanachZSW12a,
  author       = {Richard Banach and
                  Huibiao Zhu and
                  Wen Su and
                  Xiaofeng Wu},
  editor       = {John Derrick and
                  John S. Fitzgerald and
                  Stefania Gnesi and
                  Sarfraz Khurshid and
                  Michael Leuschel and
                  Steve Reeves and
                  Elvinia Riccobene},
  title        = {Continuous ASM, and a Pacemaker Sensing Fragment},
  booktitle    = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third International
                  Conference, {ABZ} 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {7316},
  pages        = {65--78},
  publisher    = {Springer},
  year         = {2012},
  url          = {https://doi.org/10.1007/978-3-642-30885-7\_5},
  doi          = {10.1007/978-3-642-30885-7\_5},
  timestamp    = {Mon, 03 Mar 2025 20:58:01 +0100},
  biburl       = {https://dblp.org/rec/conf/asm/BanachZSW12a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}