�ݺ�ߣ

IEEE 35th International Symposium on Computer
Based Medical Systems (CBMS 2022)
Policy-Based Diabetes Detection using Formal Runtime
Verification Monitors
Abhinandan Panda 1
, Srinivas Pinisetty1
, Partha Roop 2
1
Indian Institute of Technology, Bhubaneswar, India
2
University of Auckland, Auckland, New Zealand
December 5, 2022

Outline
1 Introduction
2 ECG
3 Proposed monitoring system
4 Policies Mining
5 RV Monitor
6 Experimental results & Comparison
7 Conclusion & Future Works
8 References

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
Experimental results
& Comparison
Conclusion & Future
Works
References
References
Introduction: Diabetes
• A metabolic disorder
• Lack of control or balance in blood glucose (BG)
• Type 1 diabetes (deficiency of insulin) / Type 2 diabetes (excess of
insulin)
• Hyperglycemia (very high blood glucose levels) / hypoglycemia (very
low blood glucose levels) events (normal blood glucose level 140
mg/dL).
CBMS 2022 Abhinandan Panda December 5, 2022 1/28

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Health Complications in Diabetes
Figure: Health complications in diabetes [1]

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Global Diabetic Growth
Figure: Global diabetic growth [1]

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Invasive Blood Glucose Monitoring
Figure: Invasive blood glucose monitoring [1]

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Need of non-invasive continuous monitoring of diabetes
• Severe health complications [2].
• Around 9.3% of people are affected by diabetes globally [3] .
• Tedious initial screening process
• About 45.8% of diabetes cases with cardiac complications are untreated
[4].
• Continuous diabetes monitoring technique should be adopted [5]

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Non-invasive approach: monitoring physiological signal ECG
Time
Amplitude
S
R
Q
P
Q
R
S
QRS interval
P
PR interval
P-wave
interval
QT interval
RT interval
TpTe interval
Te
RR interval
Tp
Tp
Figure: A typical ECG Signal

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
ECG in diabetes
Figure: ECG in diabetes [6]

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
ECG and Diabetes: Analysis
hypoglycemia (low blood glucose level) results in prolongation of QT
interval [christensen2010].
Hypoglycemia (low blood glucose level) associated with increased heart
rate (HR) [heger1996].
Hyperglycemia (high blood glucose level) related with reduced heart rate
variability (HRV) [singh2000].
Corrected QT dispersion and PR interval have a significant change in
hyperglycemia condition [marfella2000].
According to [nguyen2012], ECG parameters such as corrected QT
interval, PR interval, corrected RT interval, corrected TpTe interval and
heart rate (HR) can be used for identification of hypoglycemia and
hyperglycemia detection.

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Related Works
Authors Methods Accuracy
Acharya et al. [7] Nonlinear 86.0
Jian et al. [8] Higher order spectrum 79.93
Acharya et al. [9] Discrete wavelet transform 92.02
Pachori et al. [10] Empirical mode decomposition 95.63
Swapna et al. [11] Deep learning (CNN-LSTM) 95.1

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Motivation
Deep learning-based models such as CNN, RNN, LSTM, BI-LSTM,
GRU, etc. provide a good prediction accuracy, however, these models are
"black-box".
Monitor should not only be able to classify the input signals (ECG, PPG)
accurately to access the condition of a patient but also the cause of the
outcome should be explainable.
To understand further the effect of physiological signal features on
the outcome.
There is an urge for explainable monitoring models in healthcare
[reyes2020, gastounioti2020].
We propose a formal method-based framework that is correct by
construction.
We develop a formal runtime monitoring (RV) framework based on
ECG sensing for diabetes monitoring.

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Runtime Verification : Overview
Figure: Overview of the monitor based verification process

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
RV Monitor
Definition
Consider a given property φ ⊆ tw(Σ) defining the property to monitor
that is defined as TA Aφ. Function Mφ : tw(Σ) → D is a verification
monitor for φ, where D = {T, F, CT, CF} and is defined as follows, with
σ ∈ tw(Σ) denoting the current observation (a finite timed word over the
alphabet Σ):
Mφ(σ) =







T if ∀σ′
∈ tw(Σ) : σ · σ′
∈ φ
F if ∀σ′
∈ tw(Σ) : σ · σ′
̸∈ φ
CT if σ ∈ φ ∧ ∃σ′
∈ tw(Σ) : σ · σ′
̸∈ φ
CF if σ ̸∈ φ ∧ ∃σ′
∈ tw(Σ) : σ · σ′
∈ φ
Correct by construction
Satisfy impartiality and anticipation constraints (Bauer et al.[12]).

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Proposed Monitoring Approach
Raw ECG
ECG
intervals ECG
Policy
inference
ECG
Processing
Module
Data
Mining
Model
ECG
Dataset
(Diabetic,
Healthy)
Class label
(diabetes/healthy)
Figure: Policy learning framework
ECG
events True / False
(Diabetes
detection)
Inferred ECG Policies
ECG signal
ECG
Sensor
ECG
Processing
Module
RV monitor
Figure: Proposed monitoring framework

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
ECG and Diabetes Dataset
Dataset
We consider DICARDIA database [ledezma2014] of 65 subjects with:
i) 51 diabetic subjects with cardiac complications of age 57.00 ± 10.00
years
ii) 3 diabetic subjects without cardiac complications of age 49.00 ±
12.00 years
iii) 11 healthy subjects as a control group of age 50.00 ± 6.00 years.
iv) Approximately 30 min. long records.
Signal Processing
The ECG_Processing module is implemented in Python toolkit
Neurokit2 [Makowski2021].
Apply a high pass Butterworth filter and a low pass filter to remove
baseline drift and high-frequency noise from the ECG signal.
The R-peaks in ECG are extracted using the Pan-Tompkins
algorithm [13].
Wavelet analysis to detect the P-peaks, Q-peaks, R-peaks, T-peaks and
T-ends of the ECG.

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
ECG Feature extraction
Figure: Processed ECG

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Policies Mining : Decision tree
Features
ECG intervals: PR, RR, QT, TpTe and RT
Class: Healhty (H), Diabetic (diabetic, diabetic with cardiac
complications)

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
ECG Policies
• φECG1: If RR > 619 ms and PR > 127 ms and QT > 361 ms, then it is
diabetes.
• φECG2: If RR > 619 ms and PR <= 127 ms, then it indicates diabetes.
• φECG3: When RR > 528 ms and RR <= 619 ms and RT > 297.5 ms,
diabetes is present.
• φECG4: When RR > 619 ms and PR > 127 ms and PR <= 140 ms and
QT <= 361 ms, it is diabetes.
• φECG5: If RR > 401 ms and RR <= 408 ms and RT <= 297.5 ms,
then it indicates diabetes.

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Sub-policies
Each ECG policy is a combination of multiple sub-policies. For example,
to monitor policy φECG1, we monitor the intersection of the following
sub-policies.
• PECG11: The RR interval of ECG should be less than or equal to 619 ms.
• PECG12: The PR interval of ECG should be less than or equal to 127 ms.
• PECG13: The QT interval of ECG should be less than or equal to 361 ms.

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
ECG policy as Timed Automata
l0 l1 l2
Σ R
R, x := 0
ΣR
R,
x > 619
R, x ≤ 619
Σ
(a) Timed automata representing policy
PECG11
l0 l1 l2
Σ P
P, x := 0
ΣR
R,
x > 127
R, x ≤ 127
Σ
(b) Timed automata representing policy
PECG12
l0 l1 l2
Σ Q
Q, x := 0
ΣTe
T e,
x > 361
T e, x ≤ 361
Σ
(c) Timed automata representing policy
PECG13
Figure: Timed automata representing ECG policies PECG11, PECG12 and PECG13

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
RV Monitor
Definition
Consider a given property φ ⊆ tw(Σ) defining the property to monitor
that is defined as TA Aφ. Function Mφ : tw(Σ) → D is a verification
monitor for φ, where D = {T, F, CT, CF} and is defined as follows, with
σ ∈ tw(Σ) denoting the current observation (a finite timed word over the
alphabet Σ):
Mφ(σ) =







T if ∀σ′
∈ tw(Σ) : σ · σ′
∈ φ
F if ∀σ′
∈ tw(Σ) : σ · σ′
̸∈ φ
CT if σ ∈ φ ∧ ∃σ′
∈ tw(Σ) : σ · σ′
̸∈ φ
CF if σ ̸∈ φ ∧ ∃σ′
∈ tw(Σ) : σ · σ′
∈ φ
Synthesis of RV monitor from policies formalized as timed automata
following the approaches mentioned in [pinisetty2017, pinisetty2018,
Bauer:2011].

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Example: Input-output Behavior of a RV Monitor
ECG trace : [σ = (P, 30) · (Q, 150) · (R, 155) · (Te, 500) · (R, 800)]
Table: RV monitor’s behaviour for the policy φECG1
σ MφECG1(σ)
(P, 30) CT
(P, 30) · (Q, 150) CT
(P, 30) · (Q, 150) · (R, 155) CT
(P, 30) · (Q, 150) · (R, 155) · (Te, 500) CT
(P, 30) · (Q, 150) · (R, 155) · (Te, 500) · (R, 800) CF

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Sample excetion of ECG trace on RV monitor

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Experimental Results
Accuracy(%) =
TP + TN
TP + TN + FP + FN
× 100
Sensitivity(%) =
TP
TP + FN
× 100
Specificity(%) =
TN
TN + FP
× 100
Accuracy Sensitivity Specificity
RV framework 88.07% 89.36% 86.36%
Table: RV framework Performance
Table: Comparison with other works
Authors Methods Accuracy
Acharya et al. [7] Nonlinear 86.0
Jian et al. [8] Higher order spectrum 79.93
Acharya et al. [9] Discrete wavelet transform 92.02
Pachori et al. [10] Empirical mode decomposition 95.63
Swapna et al. [11] Deep learning (CNN-LSTM) 95.1
Our RV framework Policy based 88.07

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
RV Monitor on Wearable Device
Figure: RV monitor on wearable device [14]

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
Conclusion & Future Works
Conclusion
Explainable health monitoring
Correct by construction model
Future work
Testing with other datasets
Analysing other ECG features
Implementation on wearable device

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
References I
[1] Prateek Jain, Amit M Joshi, and Saraju Mohanty. “Everything you
wanted to know about noninvasive glucose measurement and
control”. In: arXiv preprint arXiv:2101.08996 (2021).
[2] American Diabetes Association. “Diagnosis and classification of
diabetes mellitus”. In: Diabetes care 37.Supplement_1 (2014),
S81–S90.
[3] Pouya Saeedi et al. “Global and regional diabetes prevalence
estimates for 2019 and projections for 2030 and 2045: Results from
the International Diabetes Federation Diabetes Atlas”. In: Diabetes
research and clinical practice 157 (2019), p. 107843.
[4] Jessica Beagley et al. “Global estimates of undiagnosed diabetes in
adults”. In: Diabetes research and clinical practice 103.2 (2014),
pp. 150–160.
[5] Melanie J Davies et al. “Management of hyperglycemia in type 2
diabetes, 2018. A consensus report by the American Diabetes
Association (ADA) and the European Association for the Study of
Diabetes (EASD)”. In: Diabetes care 41.12 (2018), pp. 2669–2701.

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
References II
[6] Jukka Lipponen et al. “Dynamic estimation of cardiac
repolarization characteristics during hypoglycemia in healthy and
diabetic subjects”. In: Physiological measurement 32 (June 2011),
pp. 649–60. doi: 10.1088/0967-3334/32/6/003.
[7] U Rajendra Acharya et al. “An integrated diabetic index using heart
rate variability signal features for diagnosis of diabetes”. In:
Computer methods in biomechanics and biomedical engineering
16.2 (2013), pp. 222–234.
[8] Lee Wei Jian and Teik-Cheng Lim. “Automated detection of
diabetes by means of higher order spectral features obtained from
heart rate signals”. In: Journal of medical imaging and health
informatics 3.3 (2013), pp. 440–447.
[9] U Rajendra Acharya et al. “Computer-aided diagnosis of diabetic
subjects by heart rate variability signals using discrete wavelet
transform method”. In: Knowledge-based systems 81 (2015),
pp. 56–64.

Introduction
ECG
Proposed monitoring
system
Policies Mining
RV Monitor
& Comparison
Conclusion & Future
Works
References
References
References III
[10] Ram Bilas Pachori et al. “An improved online paradigm for
screening of diabetic patients using RR-interval signals”. In: Journal
of Mechanics in Medicine and Biology 16.01 (2016), p. 1640003.
[11] Goutham Swapna, Soman Kp, and Ravi Vinayakumar. “Automated
detection of diabetes using CNN and CNN-LSTM network and
heart rate signals”. In: Procedia computer science 132 (2018),
pp. 1253–1262.
[12] Andreas Bauer, Martin Leucker, and Christian Schallhart. “Runtime
Verification for LTL and TLTL”. In: ACM Trans. Softw. Eng.
Methodol. 20.4 (Sept. 2011), 14:1–14:64. issn: 1049-331X.
[13] Jiapu Pan and Willis J Tompkins. “A real-time QRS detection
algorithm”. In: IEEE transactions on biomedical engineering 3
(1985), pp. 230–236.
[14] Srinivas Pinisetty et al. “Runtime enforcement of cyber-physical
systems”. In: ACM Transactions on Embedded Computing Systems
(TECS) 16.5s (2017), pp. 1–25.

�ݺ�ߣ

CBMS_Presentation (5).pdf

Recommended

More Related Content

Similar to CBMS_Presentation (5).pdf (20)

Recently uploaded (20)

CBMS_Presentation (5).pdf