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 -