|Title:||Computational model validation using a novel multiscale multidimensional spatio-temporal meta model checking approach.|
|Full text thesis:||Download.|
|Supervision:||Professor David Gilbert and Professor Nigel Saunders.|
|Commenced:||1st October 2012.|
|Submitted:||24th August 2015.|
|Defended:||9th November 2015.|
|University:||Brunel University London.|
Computational models of complex biological systems can provide a better understanding of how living systems function but need to be validated before they are employed for real-life (e.g. clinical) applications.
One of the most frequently employed in silico approaches for validating such models is model checking. Traditional model checking approaches are limited to uniscale non-spatial computational models because they do not explicitly distinguish between different scales, and do not take properties of (emergent) spatial structures (e.g. density of multicellular population) into account.
This thesis defines a novel multiscale multidimensional spatio-temporal meta model checking methodology which enables validating multiscale (spatial) computational models of biological systems relative to how both numeric (e.g. concentrations) and spatial system properties are expected to change over time and across multiple scales. The methodology has two important advantages. First it supports computational models encoded using various high-level modelling formalisms because it is defined relative to time series data and not the models used to produce them. Secondly the methodology is generic because it can be automatically reconfigured according to case study specific types of spatial structures and properties using the meta model checking approach. In addition the methodology could be employed for multiple domains of science, but we illustrate its applicability here only against biological case studies. To automate the computational model validation process, the approach was implemented in software tools, which are made freely available online. Their efficacy is illustrated against two uniscale and four multiscale quantitative computational models encoding phase variation in bacterial colonies and the chemotactic aggregation of cells, respectively the rat cardiovascular system dynamics, the uterine contractions of labour, the Xenopus laevis cell cycle and the acute inflammation of the gut and lung.
This novel model checking approach will enable the efficient construction of reliable multiscale computational models of complex systems.
- Mule - A multiscale multidimensional spatio-temporal meta model checker;
- Mudi - A multidimensional spatio-temporal model checker.
Related publications, oral presentations and posters
Ovidiu Pârvu, David Gilbert, A Novel Method to Verify Multilevel Computational Models of Biological Systems Using Multiscale Spatio-Temporal Meta Model Checking, PLOS ONE, vol. 11, no. 5, pp. 1-43, May 2016 [source code repository, website].
Ovidiu Pârvu, David Gilbert, Monika Heiner, Fei Liu, Nigel Saunders and Simon Shaw, Spatial-temporal modelling and analysis of bacterial colonies with phase variable genes, ACM Transactions On Modeling and Computer Simulation, vol. 25, no. 2, pp. 13:1–13:25, May 2015 [website].
Ovidiu Pârvu and David Gilbert, Automatic validation of computational models using pseudo-3D spatio-temporal model checking, BMC Systems Biology, vol. 8, no. 1, pp. 124, December 2014 [website].
Ovidiu Pârvu and David Gilbert, Implementation of linear minimum area enclosing triangle algorithm, Computational and Applied Mathematics, Springer, pp. 1–16, November 2014 [source code repository, website].
Ovidiu Pârvu, David Gilbert, Monika Heiner, Fei Liu, and Nigel Saunders, Modelling and Analysis of Phase Variation in Bacterial Colony Growth, In Proceedings Computational Methods in Systems Biology, 11th International Conference CMSB 2013, Springer, LNCS, vol.8130, 2013, pp 78-91 [supplementary materials].
Ovidiu Pârvu, Formally validating multidimensional computational models, 14481 Dagstuhl seminar on Multiscale Spatial Computational Systems Biology, 23rd – 28th of November, 2014, Dagstuhl, Germany.
Ovidiu Pârvu and David Gilbert, Multilevel spatial modelling using Coloured Petri Nets, 14481 Dagstuhl seminar on Multiscale Spatial Computational Systems Biology, 23rd – 28th of November, 2014, Dagstuhl, Germany.
Ovidiu Pârvu, Formal validation of multidimensional computational models, International Study Group for Systems Biology (ISGSB) 2014 meeting, Durham, United Kingdom, 1st – 5th of September, 2014 (best presentation award).
Ovidiu Pârvu, Spatial modelling and analysis of biological systems, PhD student conference on Complex Systems (CCS) 2014, Brunel University, London, United Kingdom, 27th of June, 2014 (invited speaker).
Ovidiu Pârvu, Multidimensional model verification, Doctoral colloquium of the Conference On Spatial Information Theory (COSIT) 2013, Scarborough, United Kingdom, 2nd - 6th September 2013 (best presentation award).
Presentation at the Petri Net Course Tutorial: Petri nets for multiscale systems biology workshop, University of Milano-Bicocca, Milan, Italy, 25th of June 2013.
Assisted prof. David Gilbert, Brunel University, at the Erasmus Intensive Programme Modelling in Systems and Synthetic Biology 2013 (MoSyB 2013), Latvia University of Agriculture, Jelgava, Latvia, 17th of June 2013.
Ovidiu Pârvu, David Gilbert, Monika Heiner, Fei Liu, Nigel Saunders, A systems biology approach to modelling growth and phase variation in bacterial colonies, Annual CLMS Symposium 2013, UCL Bloomsbury Campus, UCL, London, United Kingdom, 28th of June 2013 (3rd best poster award).
Ovidiu Pârvu, David Gilbert, Nigel Saunders, Spatial modelling and analysis of phase variation in bacterial colonies, Brunel University Research Student Poster Conference, 30th of April, 2013.