Prediction of inherited and genetic mutations using the software model checker SPIN

ABSTRACT

Genetic testing is becoming an important tool for detection of many genetic diseases. Designing a genetic test requires accurate data and an efficient means of comparing sequences that are present in the databases. However, as prodigious amount of data continue to emerge, querying the database to make important predictions is becoming arduous. It is essential that better tools be designed to analyze these data. In this paper, a model-based approach to gene tests and the analysis of metabolic pathways is proposed. Gene sequences and metabolic processes are modeled using formal language, and predictions are made through the verification mechanism of a software model checker. The technique is demonstrated with models of genes for cystic fibrosis tranmembrane conductance regulator protein and the map kinase pathway.

REFERENCES

• 1: Blumer, K. J. and Johnson, G. L., " Diversity in function and regulation of MAP kinase pathwasy," <u>Trends in Biochemical Sciences</u>, vol. 19, pp. 236--240, 1994.
• 2: Cobb, M. H. and Schaefer, E. M., "MAP Kinase Signaling Pathways," <u>Promega Notes Magazine</u>, vol. 59, pp. 37--41, 1996.
• 3: Holzmann, G. J., <u>The SPIN Model Checker: Primer and Reference Manual</u>, Addison-Wesley, 2003.
• 4: Huth, M. and Ryan, M., <u>Logic in Computer Science</u>, Cambridge University Press, 2001.
• 5: The International Human Genome Sequence Consortium "The initial Sequencing and Analysis of the Human Genome," <u>Nature</u>, vol. 409, pp. 860--921, 2001.
• 6: Johnson, G. L. and Lapadat, R., "Mitogen-Activated Protein Kinase Pathways Mediated by ERK, JNK, and p38 Protein Kinases," <u>Science</u>.{Online document}, 1072682. Available at http://www.sciencemag.org/cgi/content/full/298/5600/1911#FI
• 7: National Institute of Health, "Cystic Fibrosis Research Directions" NIH Publication No. 97--4200 {Online document} Feb. 1998, {2003 November 24}, Available at http://www.niddk.nih.gov/health/endo/pubs/cystic/cystic.htm.

INDEX TERMS

Keywords:
genetic testing, model checking, pharmacogenomics