I investigate formal methods for the modeling and analysis of hybrid and probabilistic systems in the area of medical cyber-physical systems (CPSs), systems and synthetic biology and system design. I'm particularly interested in the development and application of techniques for automated verification, control and synthesis of such systems, which is made challenging by quantitative aspects such as stochastic and continuous non-linear dynamics, as well as the hybrid dynamics that naturally arise in CPSs.

In my current and past research, I have worked on several case studies where providing formal correctness guarantees and correct-by-design model and controller synthesis is critical, including the artificial pancreas for closed-loop diabetes therapy, implantable cardiac devices for treatment of arrhythmias and biological networks for disease prediction and engineering of molecular devices.

Data-driven robust control for insulin therapy
Period: 2016-2017  |  Collaborators: Scott Smolka, Shan Lin, Kin Sum Liu

The artificial pancreas aims to automate treatment of type 1 diabetes (T1D) by integrating insulin pump and glucose sensor through control algorithms. However, fully closed-loop therapy is challenging since the blood glucose levels to control depend on disturbances related to the patient behavior, mainly meals and physical activity.

To handle meal and exercise uncertainties, in our work we construct data-driven models of meal and exercise behavior, and develop a robust model-predictive control (MPC) system able to reject such uncertainties, in this way eliminating the need for meal announcements by the patient. The data-driven models, called uncertainty sets, are built from data so that they cover the underlying (unknown) distribution with prescribed probabilistic guarantees. Then, our robust MPC system computes the insulin therapy that minimizes the worst-case performance with respect to these uncertainty sets, so providing a principled way to deal with uncertainty. State estimation follows a similar principle to MPC and exploits a prediction model to find the most likely state and disturbance estimate given the observations.

We evaluate our design on synthetic scenarios, including high-carbs intake and unexpected meal delays, and on large clusters of virtual patients learned from population-wide survey data sets (CDC NHANES).

Data-driven robust control for insulin therapy
Robust artificial pancreas design

SMT-based synthesis of safe and robust PID controllers

In this work, we present a new method for the automated synthesis of PID controllers with safety and performance guarantees for hybrid systems with stochastic and nonlinear dynamics. Synthesized controllers are robust by design since they minimize the probability of reaching an unsafe state under random disturbances.

It is well known that safety verification is a difficult problem (undecidable) for nonlinear hybrid systems, hence it must be solved using approximation methods. We build on the frameworks of delta-satisfiability (implemented in tools like dReal and iSAT) and probabilistic delta-reachability (ProbReach tool) to reason formally about nonlinear and stochastic dynamics by providing solutions with numerical guarantees up to an arbitrary precision.

We evaluate our approach by synthesizing provably safe and robust controllers for the artificial pancreas case study, where we manage to avoid hypoglycemia (low blood sugar) and reject large random meal disturbances.

SMT-based synthesis of safe and robust PID controllers
Blood glucose levels under basal insulin therapy (left) and synthesized controller (right).

Attacking ECG biometrics

With the increasing popularity of mobile and wearable devices biometric recognition has become ubiquitous. Unlike passwords, which rely on the user knowing something, biometrics make use of either distinctive physiological properties or behavior.

In this work, we study a systematic attack against ECG biometrics, i.e., that leverage the electrocardiogram signal of the wearer, and evaluate the attack on a commercial device, the Nymi band. We instantiated the attacks using different techinques: a hardware-based waveform generator, a computer sound card, and the playback of ECG signals encoded as .wav files using an off-the-shelf audio player.

We collected training data from 40+ participants using a variety of ECG monitors, including a medical monitor, a smartphone-based mobile monitor and the Nymi Band. Then, we enrolled users into the Nymi Band and test whether data from any of the above ECG sources can be used for a signal injection attack. Using data collected directly on the Nymi Band, we achieve a success rate of 81%, which decreases to 43% with data from other devices.

To improve the success rate with data from other devices, available to the attacker through e.g. medical records of the victim, we devise a method for learning optimal mappings between devices (using training data), i.e., functions that transforms the ECG signal of one device as if it was produced by another device. Thanks to this method, we achieved a 62% success rate with data not produced by the Nymi band.

Presentation of the work at NDSS 2017 conference

Closed-loop quantitative verification of rate-adaptive pacemakers

Rate-adaptive (RA) pacemakers are able to adjust the pacing rate depending on the levels of activity of the patient, detected by processing physiological signals data. RA pacemakers represent the only choice when the heart rate cannot naturally adapt to increasing demand (e.g. AV block). RA parameters depend on many patient-specific factors, and effective personalisation of such treatments can only be achieved through extensive exercise testing, which is normally intolerable for a cardiac patient.

We introduce a data-driven and model-based approach for the quantitative verification of RA pacemakers and formal analysis of personalised treatments. We developed a novel dual-sensor pacemaker model where the adaptive rate is computed by blending information from an accelerometer, and a metabolic sensor based on the QT interval (a feature of the ECG). The approach builds on the HeartVerify tool to provide statistical model checking of the probabilistic heart-pacemaker models, and supports model personalization from ECG data (see heart model page). Closed-loop analysis is achieved through the online generation of synthetic, model-based QT intervals and acceleration signals.

We further extend the model personalization method to estimate parameters from patient population, thus enabling safety verification of the device. We evaluate the approach on three subjects and a pool of virtual patients, providing rigorous, quantitative insights into the closed-loop behaviour of the device under different exercise levels and heart conditions.

Closed-loop quantitative verification of rate-adaptive pacemakers
Heart rate during a simulated Bruce protocol (a common clinical stress test). The ideal rate demand (blue) is compared to the heart under different adaptation algorithm configurations.

HeartVerify: Model-Based Quantitative Verification of Cardiac Pacemakers
Period: 2015-2017  |  Collaborators: Alexandru Mereacre, Marta Kwiatowska, Andrea Patane, Benoit Barbot

HeartVerify is a framework for the analysis and verification of pacemaker software and personalised heart models. Models are specified in MATLAB Stateflow and are analysed using the Cosmos tool for statistical model checking, thus enabling the analysis of complex nonlinear dynamics of the heart, where precise (numerical) verification methods typically fail.

The approach is modular in that it allows configuring and testing different heart and pacemaker models in a plug-and-play fashion, without changing their communication interface or the verification engine. It supports the verification of probabilistic properties, together with additional analyses such as simulation, generation of probability density plots (see figure) and parametric analyses. HeartVerify comes with different heart and pacemaker models, including methods for model personalization from ECG data and rate-adaptive pacing.

HeartVerify: Model-Based Quantitative Verification of Cardiac Pacemakers
Estimated probability mass function for the number of paced beats in using statistical model checking.

Hardware-in-the-loop energy optimization
Period: 2015-2016  |  Collaborators: Marta Kwiatowska, Alexandru Mereacre, Benoit Barbot, Andrea Patane, Chris Barker

Energy efficiency of cardiac pacemakers is crucial because it reduces the frequency of device re-implantations, thus improving the quality of life of cardiac patients.

To achieve effective energy optimisation, we take a hardware-in-the-loop (HIL) simulation approach: the pacemaker model is encoded into hardware and interacts with a computer simulation of the heart model. In addition, a power monitor is attached to the pacemaker to provide real-time power consumption measurements. The approach is model-based and supports generic control systems. Controller (e.g., pacemaker) and plant (e.g., heart) models are specified as networks of parameterised timed input/output automata (using MATLAB Stateflow) and translated into executable code.

We realise a fully automated optimisation workflow, where HIL simulation is used to build a probabilistic power consumption model from power measurement data. The obtained model is used by the optimisation algorithm to find optimal pacemaker parameters that e.g., minimise consumption or maximise battery lifetime. We additionally employ parameter synthesis methods to restrict the search to safe parameters. We employ timed Petri nets as an intermediate representation of the executable specification, which facilitates efficient code generation and fast simulations.

Video demonstration of HIL energy optimization

Probabilistic timed modelling of cardiac dynamics and personalization from ECG

We developed a timed automata translation of the IDHP (Integrated Dual-chamber Heart and Pacer) model by Lian et al. Timed components realize the conduction delays between functional components of the heart and action potential propagation between nodes is implemented through synchronisation between the involved components. In this way, the model can be easily extended with other accessory conduction pathways in order to reproduce specific heart conditions.

The IDHP model can be also parametrised from patient electrocardiogram (ECG) in order to reproduce the specific physiological characteristics of the individual. For this purpose, we extended the model in order to generate synthetic ECG signals that reflect the heart events occurring at simulation time. Starting from raw ECG recordings, our method automatically finds model parameters such that the synthetic signal best mimics the input ECG, by minimising the statistical distance between the two. The resulting parameters correspond to probabilistic delays in order to reflect variability of ECG features.

The IDHP heart model can be downloaded from the tool page, while personalization from ECG data is implemented in the HeartVerify tool.

Probabilistic timed modelling of cardiac dynamics and personalization from ECG
Mean input ECG (red) and mean synthetic ECG (blue) generated from the personalized model.

Parameter synthesis for pacemaker design optimization
Period: 2014-2015  |  Collaborators: Marta Kwiatowska, Alexandru Mereacre, Andrea Patane

Verification is useful in establishing key correctness properties of cardiac pacemakers, but has limitations, in that it is not clear how to redesign the model if it fails to satisfy a given property. Instead, parameter synthesis aims to automatically find optimal values of parameters to guarantee that a given property is satisfied.

In this project, we develop methods to synthesize pacemaker parameters that are safe, robust and, at the same time, able to optimise a given quantitative requirement such as energy consumption or clinical indicators. We solve this problem by combining symbolic methods (SMT solving) for ruling out parameters that violate heart safety (red areas in the figure) with evolutionary strategies for optimising the quantitative requirement.

Parameter synthesis for pacemaker design optimization
Synthesis by bilevel optimization. Right: the maximal robust parameter (blue) is the center of the largest cube (light blue) without counter-examples (red). Left: in a bilevel problem, the domain of the outer problem is the solution space of the inner problem.