Verificação Formal aplicada a Biologia Sistêmica

Nesse projeto utilizamos ferramentas de verificação formal probabilística para modelar e analisar sistemas biológicos e entender melhor seu comportamento. O uso de métodos formais nos permite criar modelos que podem descobrir eventos raros, porém importantes, que seriam de outro modo ignorados.

Este projeto conta a colaboração de Jáder Cruz, professor do Departamento de Bioquímica e Imunologia da Universidade Federal de Minas Gerais.

Atualmente, estamos estudando sistemas de transporte de íons através da membrana das células, tais como bombas e canais de iônicos, e como eles reagem à presença de toxinas. Esses sistemas são importantes estruturas celulares que podem colocar em risco um indivíduo se o seu comportamento normal for comprometido. Algumas toxinas tais como a Palitoxina podem comprometer o comportamento normal da bomba de íons, essencialmente transformando-a em um canal de íon.

Foram construídos três modelos formais para o verificador de modelos PRISM (http://www.prismmodelchecker.org/). Cada modelo representa um aspecto das interações da palitoxina com a bomba de sódio e potássio, listados a seguir (no link é possível fazer o download do modelo e das propriedades formais elaboradas).

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

Nesta etapa do projeto foi produzida a seguinte dissertação de mestrado por Fernando Braz, orientado por Sérgio Campos e co-orientado por 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.

Anteriormente, neste projeto foi proposto o primeiro modelo formal do ciclo da bomba de sódio e potássio, onde foram estudadas diferentes formas de modelar a mesma utilizando as ferramentas PRISM e BioLab. Nesta etapa do projeto foi produzida a seguinte dissertação de mestrado por Mirlaine Crepalde, orientada por Sérgio Campos e co-orientada por 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.

Publicações

Neste projeto foram publicados dois periódicos, três artigos e cinco resumos, relacionados abaixo. Além disso, duas ferramentas foram desenvolvidas, listadas mais abaixo.

(Periódicos)

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

Artigo final: ainda não disponível
Pre-Print do artigo: 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.

Versão final: http://www.biomedcentral.com/1471-2164/12/S4/S14

(Artigos)

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.

Versão final: ainda não disponível
Rascunho: ainda não disponível
Slides da apresentação: ainda não disponível

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.

Versão final: http://link.springer.com/chapter/10.1007/978-3-642-33296-8_5
Rascunho: http://fernandoafb.files.wordpress.com/2012/10/sbmf2012-final.pdf
Slides da apresentação: 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.

Versão final: http://link.springer.com/chapter/10.1007%2F978-3-642-31927-3_8
Rascunho: http://fernandoafb.files.wordpress.com/2012/08/bsb2012.pdf
Slides da apresentação: http://fernandoafb.files.wordpress.com/2012/08/slidesbsb2012.pdf

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.

(Resumos)

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.

Resumo: 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.

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

(Ferramentas)

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