Continuous ASM, and a pacemaker sensing fragment

Richard Banach; Huibiao Zhu; Wen Su; Xiaofeng Wu

doi:10.1007/978-3-642-30885-7_5

Continuous ASM, and a pacemaker sensing fragment

Richard Banach, Huibiao Zhu, Wen Su, Xiaofeng Wu

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

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. © 2012 Springer-Verlag.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Publisher	Springer Nature
Pages	65-78
Number of pages	13
Volume	7316
ISBN (Print)	9783642308840
DOIs	https://doi.org/10.1007/978-3-642-30885-7_5
Publication status	Published - 2012
Event	3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012 - Pisa Duration: 1 Jul 2012 → …

Conference

Conference	3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012
City	Pisa
Period	1/07/12 → …

Access to Document

10.1007/978-3-642-30885-7_5

Cite this

@inproceedings{00e44e28280e4a1584cde7b95c18d323,

title = "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. {\textcopyright} 2012 Springer-Verlag.",

author = "Richard Banach and Huibiao Zhu and Wen Su and Xiaofeng Wu",

year = "2012",

doi = "10.1007/978-3-642-30885-7_5",

language = "English",

isbn = "9783642308840",

volume = "7316",

pages = "65--78",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

publisher = "Springer Nature",

address = "United States",

note = "3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012 ; Conference date: 01-07-2012",

}

Banach, R, Zhu, H, Su, W & Wu, X 2012, Continuous ASM, and a pacemaker sensing fragment. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 7316, Springer Nature, pp. 65-78, 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012, Pisa, 1/07/12. https://doi.org/10.1007/978-3-642-30885-7_5

Continuous ASM, and a pacemaker sensing fragment. / Banach, Richard; Zhu, Huibiao; Su, Wen et al.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 7316 Springer Nature, 2012. p. 65-78.

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Continuous ASM, and a pacemaker sensing fragment

AU - Banach, Richard

AU - Zhu, Huibiao

AU - Su, Wen

AU - Wu, Xiaofeng

PY - 2012

Y1 - 2012

N2 - 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. © 2012 Springer-Verlag.

AB - 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. © 2012 Springer-Verlag.

U2 - 10.1007/978-3-642-30885-7_5

DO - 10.1007/978-3-642-30885-7_5

M3 - Conference contribution

SN - 9783642308840

VL - 7316

SP - 65

EP - 78

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

PB - Springer Nature

T2 - 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012

Y2 - 1 July 2012

ER -

Continuous ASM, and a pacemaker sensing fragment

Abstract

Conference

Access to Document

Fingerprint

Cite this