D. Naujokaitis “Hybrid systems modelling using aggregate method and them verification” doctoral thesis defence

Author, Institution: Darius Naujokaitis, Kaunas University of Technology

Science area, field of science: Physical Sciences, Informatics, 09P

Doctoral thesis was prepared externally.

Scientific Advisor: Prof. Dr. Habil. dr. Rimantas Barauskas (Kaunas University of Technology,
Physical Sciences, Informatics – 09P, 2018)
Scientific Supervisor: Prof. Dr. Habil. Henrikas Pranevičius (Kaunas University of Technology,
Physical Sciences, Informatics – 09P, 2010-2015)

Dissertation Defence Board of Informatics Science Field:
Prof. Dr. Vacius Jusas (Kaunas University of Technology, Physical Sciences, Informatics – 09P) – chairman;
Prof. Dr. Habil. Gintautas Dzemyda (Vilnius University, Physical Sciences, Informatics – 09P);
Prof. Dr. Gintaras Palubeckis (Kaunas University of Technology, Physical Sciences, Informatics – 09P);
Assoc. Prof. Dr. Kristina Poškuvienė (Kaunas University of Technology, Physical Sciences, Informatics – 09P);
Prof. Dr. Jüri Vain (Tallinn University of Technology, Estonia, Physical Sciences, Informatics – 09P).

The doctoral dissertation is available at the library of Kaunas University of Technology (K. Donelaičio St. 20, Kaunas).

Annotation:

In the thesis hybrid systems, consisting of discrete and continuous components and describing the individual parts of the human physiological system, are modeled by aggregate formalization method that includes tools for simulation and testing of created models.
In the dissertation there is investigated created original models, which are formalized by an aggregate method, investigating the collateral circulatory system of the human brain and pharmacokinetic phenomena. Simulation models for collateral blood flow are based on electrical chain and they simulate impact of regional cerebral blood flow (rCBF) to regional cerebral perfusion pressure (rCPP) imitating blood vessel contraction in the case of stroke. The developed pharmacokinetic model allows assessing the effect of opioid concentrations on the patient based on the assessment of the degree of pain and the potential side effects of opioids.
The new method of verification of aggregate models proposed in the dissertation is based on the semantic equivalence of aggregate and stochastic hybrid automata models in the time transition system and allows automated verification of such models. Using this method, the pharmacokinetic model was tested using the UPPAAL-SMC verification tool supplemented by statistical model checking techniques.