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.

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).

Robust design synthesis for probabilistic systems
Period: 2016-2017  |  Collaborators: Radu Calinescu, Simos Gerasimou, Milan Ceska, Marta Kwiatowska

We consider the problem of synthesizing optimal and robust designs (given as parametric Markov chains) that are 1) robust to pre-specified levels of variation in the system parameters; 2) satisfy strict performance, reliability and other quality constraints; and 3) are Pareto optimal with respect to a set of quality optimisation criteria.

The resulting Pareto front consists of quality attribute regions induced by the parametric designs (see picture). The size and shape of these regions provide key insights into the system robustness since they capture the sensitivity of quality attributes to parameter changes (i.e, small regions = robust designs).

The method is implemented in the RODES tool and is based on a combination of GPU-accelerated parameter synthesis for Markov chains (to compute the quality attribute regions for fixed discrete parameters) through the PRISM-PSY tool, and multi-objective optimization based on an extended, sensitivity-aware dominance relation.

Robust design synthesis for probabilistic systems
Sensitivity-aware Pareto front for the Google File System model. Through an extended Pareto dominance relation we can include designs that are slightly suboptimal but with improved robustness (in red).

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

Precise parameter synthesis for continuous-time Markov chains
Period: 2014-2016  |  Collaborators: Milan Ceska, Marta Kwiatowska, Frits Dannenberg, Peter Pilar, Lubos Brim

Given a parameteric continuous-time Markov chain (pCTMC), we aim at finding parameter values such that a CSL property is guaranteed to hold (threshold synthesis), or, in the case of quantitative properties, the probability of satisfying the property is maximised or minimised (max synthesis).

The solution of the threshold synthesis (see picture) is a decomposition of the parameter space into true and false regions that are guaranteed to, respectively, satisfy and violate the property, plus an arbitrarily small undecided region. On the other hand, in the max synthesis problem we identify an arbitrarily small region guaranteed to contain the actual maximum/minimum.

We developed synthesis methods based on a parameteric extension of probabilistic model checking to compute probability bounds, as well as refinement and sampling of the parameter space. We implemented GPU-accelerated algorithms for synthesis in the PRISM-PSY tool, which we applied to a variety of biological and engineered systems, including models of molecular walkers, mammalian cell cycle, and the Google file system.

Precise parameter synthesis for continuous-time Markov chains
Parameter ranges and bounds (vertical axis) for the probability of infection extinction in an epidemic model. Green: true region, i.e., with probability above the desired threshold (transparent plane). Red: false region. Yellow: undecided region.

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

A multi-level model for self-adaptive systems
Period: 2012-2015  |  Collaborators: Emanuela Merelli, Luca Tesei

Self-adaptive systems are able to modify their own behaviour according to their environment and their current configuration, in order to fulfil an objective, to better respond to problems, or maintain desired conditions.

In this project, we introduce a hierarchical approach to formal modelling and analysis of self-adaptive systems. It is based on a structural level S, describing the adaptation dynamics of the system, and a behavioural level B describing the admissible dynamics of the system. The S level imposes structural constraints on the B level, which has to adapt whenever it no longer can satisfy them (top-down adaptation).

We introduce weak and strong adaptability relations, capturing the ability of a system to adapt for some evolution paths or for all possible evolutions, respectively, and show that adaptability checking, i.e. deciding if a system is weak or strong adaptable, can be reduced to a CTL model checking problem.

A multi-level model for self-adaptive systems
Hyper-graph representation of a self-adaptive system with three levels. Black dots are states at the first level, called the behavioral level. The higher level, called structural level, defines adaptation dynamics. A state in the structural level corresponds to sets of stable states in the behavioral level. Adaptation occurs whenever the system transitions to a different structural state. The same hierarchical dynamics can be extended to multiple levels.