Formal Verification Applied to Systems Biology

In this project we use probabilistic formal verification tools to model and analyze biological systems in order to improve our understanding of their behavior. Formal methods allow us to create models which can find rare but important events, which would be ignored otherwise.

This project has the support of Jáder Cruz, prof. of the Department of Biochemistry and Immunology at Universidade Federal de Minas Gerais.

Currently, we are studying ionic transport systems through the cell membrane, such as pumps and ion channels, and how they react to the presence of toxins. These systems are important cell structures which can cause diseases or syndromes if their regular behavior is compromised. Some toxins such as Palytoxin can disrupt an ionic pump, turning it into an ion channel.

Three formal models have been built for the PRISM model checker (http://www.prismmodelchecker.org/). Each model represents one aspect of the palytoxin interactions with the sodium potassium pump, listed below (the link allows the download of the formal model and properties).

ptx2007: http://homepages.dcc.ufmg.br/~fbraz/bsb2012/
ptx2008a: http://homepages.dcc.ufmg.br/~fbraz/sbmf2012/
ptx2008b: http://homepages.dcc.ufmg.br/~fbraz/bsb2013/

This stage of the project produced the following Master’s thesis by Fernando Braz, advised by Sérgio Campos and co-advised by Alessandra Faria-Campos:

Braz, F. A. F.. Probabilistic Model Checking for Modeling and Analysis of Toxins Interactions with Transmembrane Ionic Transport Systems, Dissertação de Mestrado, Universidade Federal de Minas Gerais, Belo Horizonte, 2013.

Previously, in this project it was proposed the first formal model of the sodium potassium, where different modeling approaches have been studied using the PRISM and BioLab tools. During this stage of the project, the following Master’s thesis has been produced by Mirlaine Crepalde, advised by Sérgio Campos and co-advised by Alessandra Faria-Campos:

Crepalde, M.. Modelagem e análise de sistemas de transporte de íons em membranas celulares usando verificação de modelos. Dissertação de Mestrado, Universidade Federal de Minas Gerais, Belo Horizonte, 2011.

Publications

In this project, two journals, three papers and five abstracts have been published, listed below. Additionally, two tools have been developed, listed further below.

(Journals)

Fernando A. F. Braz, Jader S. Cruz, Alessandra C. Faria-Campos, Sergio V. A. Campos, Probabilistic Model Checking Analysis of Palytoxin Effects on Cell Energy Reactions of the Na+/K+-ATPase, IEEE/ACM Transactions on Computational Biology and Bioinformatics, vol. 99, no. PrePrints, p. 1, , 2013

Final version: ainda não disponível
Pre-Print: http://www.computer.org/csdl/trans/tb/preprint/06579609-abs.html

CREPALDE, M. A. ; FARIACAMPOS, Alessandra C ; Campos, Sérgio V.A. . Modeling and analysis of cell membrane systems with probabilistic model checking. BMC Genomics, v. 12, p. S14, 2011.

Final version: http://www.biomedcentral.com/1471-2164/12/S4/S14

(Papers)

Fernando Braz, João Amaral, Bruno Ferreira, Jader Cruz, Alessandra C. Faria-Campos and Sergio Campos: A Probabilistic Model Checking Analysis of the Potassium Reactions with the Palytoxin and Na+/K+-ATPase Complex, Full paper published and accepted for oral presentation at BSB (Brazilian Symposium on Bioinformatics), Recife, 2013.

Final version: not yet available
Draft: not yet available
Presentation slides: not yet available

Fernando A. F. Braz, Jader S. Cruz, Alessandra C. Faria-Campos, Sérgio V. A. Campos: Palytoxin Inhibits the Sodium-Potassium Pump – An Investigation of an Electrophysiological Model Using Probabilistic Model Checking, Full paper published and accepted for oral presentation at SBMF (Brazilian Symposium on Formal Methods), Natal, 2012.

Final version: http://link.springer.com/chapter/10.1007/978-3-642-33296-8_5
Draft: http://fernandoafb.files.wordpress.com/2012/10/sbmf2012-final.pdf
Presentation slides: http://fernandoafb.files.wordpress.com/2012/10/slidessbmf2012.pdf

Fernando A. F. Braz, Jader S. Cruz, Alessandra C. Faria-Campos, Sérgio V. A. Campos: A Probabilistic Model Checking Approach to Investigate the Palytoxin Effects on the Na+/K+-ATPase, Full paper published and accepted for oral presentation at BSB (Brazilian Symposium on Bioinformatics), Campo Grande, 2012.

Final version: http://link.springer.com/chapter/10.1007%2F978-3-642-31927-3_8
Draft: http://fernandoafb.files.wordpress.com/2012/08/bsb2012.pdf
Presentation slides: http://fernandoafb.files.wordpress.com/2012/08/slidesbsb2012.pdf

(Abstracts)

Braz, F. A. F., Cruz, J. S., Faria-Campos, A. C., Campos, S. V. A.: Model and Analysis of Palytoxin Interactions with Sodium-Potassium Pump Using Probabilistic Model Checking, Abstract accepted for poster presentation at SBECEL (Simpósio Brasileiro de Eletrofisiologia Celular), Belo Horizonte, 2012.

Abstract: http://fernandoafb.files.wordpress.com/2012/06/abstract_sbecel2012_fernandoaugustofernandesbraz.pdf
Poster: http://fernandoafb.files.wordpress.com/2012/06/sbecel_poster_v1.pdf

Braz, F. A. F., Faria-Campos, A. C., Campos, S. V. A.: Analyzing Palytoxin Interactions with Na+/K+-ATPase Using Probabilistic Model Checking, Abstract accepted for poster presentation at X-Meeting, Florianópolis, 2011.

Abstract: http://fernandoafb.files.wordpress.com/2011/10/xmeeting2011_abstract.pdf
Poster: http://cdn.f1000.com/posters/docs/66703780

CREPALDE, M. A. ; Faria-Campos, A. ; Campos, S . Modelling and Analysing Membrane Systems with Probabilistic Model Checking. In: 6th International Conference of the Brazilian Association of Bioinformatics and Computational Biology, 2010, Ouro Preto. X-Meeting Eletronic Abstracts Book 2010, 2010.

CREPALDE, M. A. ; Faria-Campos, A. ; Campos, S . Modeling and Analysis of Sodium Potassium Exchange Pump with Probabilistic Model Checking. In: Brazil Deutschland Systems Biology Meeting, 2010, Ouro Preto. SB-meeting Eletronic Abstracts Book 2010, 2010.

CREPALDE, M. A. ; Faria-Campos, A. ; Campos, S . Modelling Ion Channels Using Symbolic Model Checking. In: 5th International Conference of the Brazilian Association of Bioinformatics and Computational Biology, 2009, Angra dos Reis. X-Meeting Eletronic Abstracts Book 2009, 2009.

(Tools)

dot2heatmap – https://code.google.com/p/dot2heatmap/
MCHelper – https://code.google.com/p/mchelper