Medical-Cyber-Physical-System

⚠️ Warning

Important: This repository contains medical jargon and electrophysiological terms. Please ensure you have the necessary knowledge and expertise before proceeding.

Heart Model

A Patient-specific heart model simulation from mlab-upenn research group

Chosen Model

Mlab-Penn team says:

**Timed automata vs. other formalisms**
We chose Timed Automata as the formalism for the heart model for several reasons:
    1. Nondeterminism which enables model abstraction which increases coverage.
    2. The reachability problem for timed automata is decidable, allowing us to explore the whole state space of the heart and pacemaker.
    Most timing behaviors of the heart can be captured by timed automata


**The proper level of abstraction: Coverage vs. Expressiveness**
To be used in different stages during the development process, the structure and parameters of our heart model need to be adjusted to balance between Coverage vs. Expressiveness.
Intuitively, the more complex the model is, there are more constraints on its behaviours, thus limiting its coverage. On the other hand, the added complexity allows us to capture more detailed mechanisms of the heart, allowing us to precisely model a specific heart condition. So instead of developing a single heart model, we developed a series of heart models at different abstraction levels. With the Counter-Example-Guided Abstraction & Refinement (CEGAR) framework, we can choose the proper level of heart model abstraction during verification thus balancing coverage and expressiveness.

Abstract conduction delay with paths

In this abstraction, we replace the *cond* state of N0 with path automata. The heart model H0 can be replaced by

. A more general abstraction abstracts 3 nodes and 2 paths into 2 nodes and 1 path:

. With this property, we can further abstract the structure of the model. The heart model H0.5 can be further abstracted into

where m=9 in the structure shown on the right.

Proposed use:

• Study heart conditions with additional pathways including reentry circuits.
• Patient-specific heart model for general Electrophysiology Study.

Node States

The components of the cardiac action potential cycle, include the periods of rest, conduction, ERP (Effective Refractory Period), RRP (Relative Refractory Period), and the rest (diastolic) period.

Cases [patient-specific]

1. 09/04/2011: Atrioventricular Nodal Reentry Tachycardia (AVNRT)
2. 13/04/2011: Atrial Flutter
3. 13/04/2011: Wenckebach-type A-V nodal response

This can be chosen by setting -DCASE=1,2,3 in the CMakeLists.txt file or on the command line when running CMake.

Building instructions

Requirements

• GCC
• CMake
• Qt/QML (C++/QML)
• python3 (required only if you want to generate .hpp files from .mat files)
  • scipy

Bash commands

You can use CMake vs code extension or from the root directory of the project, run the following commands:

Windows

mkdir build
cmake -Bbuild -G "MinGW Makefiles"
cmake --build build --config Debug --target all -j 10 --
build\MyHeart.exe                                       

Linux

mkdir build
cmake --build build --config Debug --target all --

Then the bin file will be in the bin directory.

Code generation (optional)

python3 case_studies/gen.py ./inc

Credits

• Mlab-upenn team

• Dr Gehad AlKady

• Dr Waheed Essam

• The contributors

  

  Images made with contrib.rocks.

TODOs (Probably will not DO them)

• Remove the values copied in the heart_automaton() and rely on the pass-by-reference
• Add features for the GUI
• Add a peacemaker model