The advance of biomedical engineering has promoted the design of new and revolutionary biomedical devices.
The purpose of such devices is to improve the quality of life in patients affected by different kinds of diseases by making the treatments they follow completely, or partially, automated. As one would expect, the more the effects of a biomedical device are relevant on health, the more the consequences due to a possible malfunction are critical. For instance, the artificial pancreas is a safety-critical device for blood glucose levels monitoring and regulation in patients with Type 1 Diabetes Mellitus (T1DM). If not correctly designed, the artificial pancreas has the capability to lead a patient to coma or worst, to death. As a consequence, design and evaluation of biomedical devices is often a long and expensive process also involving clinical experimentations with human volunteers (i.e., clinical trials).
In this setting, In Silico Clinical Trials (ISCT), i.e., clinical experimental campaigns carried out by means of computer simulations, hold the promise to decrease time and cost for the safety and efficacy assessment of biomedical devices.
The goal of this project is to perform In Silico Clinical Trials (ISCT) of software-controlled biomedical devices through model checking-driven simulations.
This project has a strong innovation potential, as it will show that an actual complex medical device can
be effectively verified in silico on hundreds of thousands of Virtual Patients (VPs) using High Performance
Computing (HPC) infrastructures available today. As a comparison, the very same artificial pancreas that we plan to verify in silico has been tested in an actual clinical trial involving only 10 (human) patients [17].
At a more general level, approaches to in silico verification of medical devices such the one carried out in
this project are likely to disclose entirely new possibilities to speed-up the current clinical trials procedures (at least in their early stages). To this end, it is worth mentioning that a mathematical model of human glucose regulation in diabetic patients [5] has been recently approved by the FDA for preclinical trials of certain insulin treatments.
Bibliography
[1] Avicenna Project. In silico clinical trials: How computer simulation will transform the biomedical industry. http://avicenna-isct.org/wp-content/uploads/2016/01/AvicennaRoadmapPDF-2..., 2016.
[2] M. Bächler, D. Menshykau, Ch. De Geyter, and D. Iber. Species-specific differences in follicular antral sizes result from diffusion-based limitations on the thickness of the granulosa cell layer. Mol. Hum. Reprod., 20(3), 2014.
[3] C. Cobelli, E. Renard, and B. Kovatchev. Artificial pancreas: Past, present, future. Diabetes, 60, 2011.
[4] L.G.E. Cox, S. Loerakker, M.C.M. Rutten, B.A.J.M. De Mol, and F.N. Van De Vosse. A mathematical
model to evaluate control strategies for mechanical circulatory support. Artif. Organs, 33(8), 2009.
[5] C. Dalla Man, F. Micheletto, D. Lv, M. Breton, B. Kovatchev, and C. Cobelli. The uva/padova type 1
diabetes simulator: New features. JDST, 8, 2014.
[6] H. De Jong. Modeling and simulation of genetic regulatory systems: A literature review. J. Comp. Biol.,
9, 2002.
[7] R. Hovorka, V. Canonico, L.J. Chassin, U. Haueter, M. Massi-Benedetti, M. Orsini Federici, T.R. Pieber,
H.C. Schaller, L. Schaupp, and T. Vering. Nonlinear model predictive control of glucose concentration in
subjects with type 1 diabetes. Physiol. Meas., 25, 2004.
[8] B. Ingalls and P. Iglesias. Control Theory and Systems Biology. MIT, 2009.
[9] S.S. Kanderian, S. Weinzimer, G. Voskanyan, and G.M. Steil. Identification of intraday metabolic profiles
during closed-loop glucose control in individuals with type 1 diabetes. JDST, 3, 2009.
[10] T. Mancini, F. Mari, A. Massini, I. Melatti, F. Merli, and E. Tronci. System level formal verification via
model checking driven simulation. In Proc. CAV 2013, volume 8044 of LNCS. Springer, 2013.
[11] T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. Anytime system level verification via parallel
random exhaustive hardware in the loop simulation. Microprocessors and Microsystems, 41, 2016.
[12] T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. SyLVaaS: System level formal verification as a
service. Fundam. Inform., 1¿2, 2016.
[13] T. Mancini, E. Tronci, I. Salvo, F. Mari, A. Massini, and I. Melatti. Computing biological model parameters
by parallel statistical model checking. In Proc. IWBBIO 2015, volume 9044 of LNCS. Springer, 2015.
[14] S. Röblitz, C. Stötzel, P. Deuflhard, H.M. Jones, D.-O. Azulay, P. van der Graaf, and S.W. Martin. A
mathematical model of the human menstrual cycle for the administration of GnRH analogues. J. Theor.
Biol., 321, 2013.
[15] P.P. Roy and K. Roy. Molecular docking and qsar studies of aromatase inhibitor androstenedione derivatives. J. Pharm. Pharmacol, 62(12):1717¿1728, 2010.
[16] S. Sinisi. Formalising biological knowledge for health-care virtual physiological human models by means of
hybrid systems.
[17] G.M. Steil, K. Rebrin, C. Darwin, F. Hariri, and M.F. Saad3. Feasibility of automating insulin delivery
for the treatment of type 1 diabetes. Diabetes, 55, 2006.
[18] E. Tronci, T. Mancini, I. Salvo, S. Sinisi, F. Mari, I. Melatti, A. Massini, F. Davì, T. Dierkes, R. Ehrig,
S. Röblitz, B. Leeners, T. H. C. Krüger, M. Egli, and F. Ille. Patient-specific models from inter-patient
biological models and clinical records. In Proc. FMCAD 2014. IEEE, 2014.
[19] D.J. Wilkinson. Stochastic Modelling for Systems Biology, Second Edition. Chapman & Hall/CRC Math.
& Comp. Biol. CRC, 2011.
[20] Verification and Validation in Computational Modelling of Medical Devices, V&V 40, ASME, https://cstools.asme.org/csconnect/CommitteePages.cfm?Committee=100108782
[21] N.R. Hill, P.C. Hindmarsh, R.J. Stevens, I.M. Stratton, J.C. Levy, and D.R. Matthews. A method for assessing quality of control from glucose profiles. Diabetic Medicine, 24:753¿758, 2007.