Abstract:
Parkinson’s disease (PD) is a neurological disorder that affects dopaminergic
nerve cells in a specific area of brain called substantia nigra. PD symptoms
include muscle rigidity, tremors, and changes in speech and gait. There is no
cure for PD but surgical treatments, i.e., Deep Brain Stimulation (DBS), can
help in relieving PD symptoms. Traditionally, DBS is done in an open-loop
manner, where stimulation/pacing is always ON, irrespective of the patient
need. As a consequence, patients can feel some side effects due to the con tinuous high frequency stimulation. Therefore, closed-loop DBS is preferred
as it allows adjusting stimulation according to the patient need, and it con sumes less power as compared to open-loop DBS. However, selection of an
appropriate biomarker for closing the feedback loop is a major challenge in
close-loop DBS. In this thesis, we propose to utilize model checking, i.e., a
formal verification technique used to exhaustively explore the complete state
space of a system, for analyzing DBS controllers. We model the basal ganglia
(BG) region from hybrid automaton to timed automata using timed abstrac tion. Thereafter, we analyze the timed automata of the closed-loop DBS
controller in response to the BG model. Furthermore, we formally verified
the closed-loop DBS using timed computation tree logic (TCTL) properties,
i.e., safety, liveness and deadlock. We show that closed-loop DBS significantly
outperforms existing open-loop DBS controller in terms of energy efficiency.
In order to demonstrate the practical effectiveness of our work, we formally
analyze the closed-loop DBS for power efficiency and time behavior with two
different algorithms, i.e., Algorithms A and B. Our results demonstrate that
the closed-loop DBS running the Algorithm B is efficient in terms of time and
power as compared to Algorithm A but stability is not always guaranteed in
Algorithm B.
