Invited Speakers

Gilles BERNOT

A genetically modified Hoare logic that identifies the parameters of a gene network

The main difficulty when modelling gene networks is the identification of the numerous parameters that govern the dynamics. Here, we are interesting in caracterizing the set of all parameter values that are consistent with observed behaviours of the gene network and we present a new approach based on Hoare logic and an associated weakest precondition calculus (a la Dijkstra) that generates constraints on the parameter values. Once proper specifications are extracted from biological traces (e.g. based on transcriptomic data), they play a role similar to programs in the classical Hoare logic. We will firstly explain the framework of genetic network models defined by René Thomas. Then, we define the Hoare/Dijkstra method, properly extended to genetic state graphs, that extracts the weakest precondition on parameter values. The method is correct and complete w.r.t. the Thomas' semantics.

David FELL

Perspectives on Genome Scale Modelling of Metabolism

Genome scale metabolic modelling is arguably the most successful current methodology at predicting a complex phenotype from genome sequences. Essentially it uses linear programming to predict optimal distributions of fluxes in a metabolic network reconstructed from a genome annotation, subject to constraints established from the requirement for mass balance in cellular metabolism in a dynamic steady state. The methodology, generally known as flux balance analysis (FBA) has increasing application in biotechnology and medicine. However, as the number of organisms and processes being modelled expands, new issues emerge that require innovation in model construction and analysis, and some methodologies that were developed for analysis of optimal microbial growth are less suitable for use in other contexts. In addition, there remain issues of data representation and interpretation in the bionformatic and metabolic databases used in model construction that provide traps for the unwary and frustrate attempts at completely automated model building. Finally there are some persistent biochemical errors that are maintained by inheritance from older models.

David HAREL

More Thoughts on the Whole Organism Challenge

In 2002 I proposed a long-term “grand challenge” for the comprehensive and realistic modeling of biological systems, where we try to understand and analyze an entire system in detail, utilizing in the modeling effort all that is known about it. The proposal was to produce an interactive, dynamic, computerized model of an entire multi-cellular organism. Specifically, I suggested the C. elegans nematode, which is extremely complex despite its small size, but well-defined in terms of anatomy and genetics. In this talk I will review this challenge, and discuss some insights about its feasibility, based on some recent modeling efforts we have carried out, including the organogenesis of the pancreas, rat neural whisking, cancer tumor formation, and various projects regarding C. elegans.

Marta KWIATKOWSKA

Estimation and Verification of Hybrid Heart Models for Personalised Medical and Wearable Devices

We are witnessing a huge growth in popularity of wearable and implantable devices equipped with sensors that are capable of monitoring a range of physiological processes and communicating the data to smartphones or to medical monitoring devices. Applications include not only medical diagnosis and treatment, but also biometric identification and authentication systems. An important requirement is personalisation of the devices, namely, their ability to adapt to the physiology of the human wearer and to faithfully reproduce the characteristics in real-time for the purposes of authentication or optimisation of medical therapies. In view of the complexity of the embedded software that controls such devices, model-based frameworks have been advocated for their design, development, verification and testing.
In this paper, we focus on applications that exploit the unique characteristics of the heart rhythm. We introduce a hybrid automata model of the electrical conduction system of a human heart, adapted from Lian et al., and present a framework for the estimation of personalised parameters, including the generation of synthetic ECGs from the model. We demonstrate the usefulness of the framework on two applications, ensuring safety of a pacemaker against a personalised heart model and ECG-based user authentication.