arrow
Return

A Continuous ASM Modelling Approach to Pacemaker Sensing

delete2014-10-07
delete5
delete
OA
AI
R
Richard Banach *
H
Huibiao Zhu
W
Wen Su
X
Xiaofeng Wu
DOI:10.1145/2610375delete
deleteOriginal
deleteShare
deleteSave
View PDF
Abstract

Abstract

En 中文
The cardiac pacemaker system, proposed as a problem topic in the Verification Grand Challenge, offers a range of difficulties to address for formal specification, development, and verification technologies. We focus on the sensing problem, the question of whether the heart has produced a spontaneous heartbeat or not. This question is plagued by uncertainties arising from the often unpredictable environment that a real pacemaker finds itself in. We develop a time domain tracking approach to this problem, as a complement to the usual frequency domain approach most frequently used. We develop our case study in the continuous ASM (Abstract State Machine) formalism, which is briefly summarised, through a series of refinement and retrenchment steps, each adding new levels of complexity to the model.
Keywords:
Verification
Theory
Design
Algorithms
Continuous ASM
rigorous design and development
cardiac pacemakers
sensing
AI Summary

AI Summary

Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.

Journal

A
ACM Transactions on Software Engineering and Methodology
IF:
6.2
Papers:
1.2K
Citations:
3.4K

Organization

E
east china normal university
Scholars:
3.1W
Papers: 2.1W
Citations: 25
U
University of Manchester
Scholars:
5.7W
Papers: 5.2W
Citations: 7.4W
S
shanghai university
Scholars:
3.9W
Papers: 2.7W
Citations: 52
researcher View more organizations