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

^*Corresponding author for this work

Software Engineering Institute

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

4 Scopus citations

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.

Original language	English
Title of host publication	Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Proceedings
Pages	65-78
Number of pages	14
DOIs	https://doi.org/10.1007/978-3-642-30885-7_5
State	Published - 2012
Event	3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012 - Pisa, Italy Duration: 18 Jun 2012 → 21 Jun 2012

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7316 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012
Country/Territory	Italy
City	Pisa
Period	18/06/12 → 21/06/12

Access to Document

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

Cite this

Banach, R., Zhu, H., Su, W., & Wu, X. (2012). Continuous ASM, and a pacemaker sensing fragment. In Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Proceedings (pp. 65-78). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7316 LNCS). https://doi.org/10.1007/978-3-642-30885-7_5

@inproceedings{55e72b01f8ac4c94b1abd88f1a980118,

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.",

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

year = "2012",

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

language = "英语",

isbn = "9783642308840",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "65--78",

booktitle = "Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Proceedings",

note = "3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012 ; Conference date: 18-06-2012 Through 21-06-2012",

}

Banach, R, Zhu, H, Su, W & Wu, X 2012, Continuous ASM, and a pacemaker sensing fragment. in Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7316 LNCS, pp. 65-78, 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012, Pisa, Italy, 18/06/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.
Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Proceedings. 2012. p. 65-78 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7316 LNCS).

Research output: Chapter in Book/Report/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.

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.

UR - https://www.scopus.com/pages/publications/84863919921

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

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

M3 - 会议稿件

AN - SCOPUS:84863919921

SN - 9783642308840

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 65

EP - 78

BT - Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Proceedings

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

Y2 - 18 June 2012 through 21 June 2012

ER -

Continuous ASM, and a pacemaker sensing fragment

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this