Toward Verified Biological Models Export

@article{citeulike:2792195, abstract = {The last several decades have witnessed a vast accumulation of biological data and data analysis. Many of these data sets represent only a small fraction of the system's behavior, making the visualization of full system behavior difficult. A more complete understanding of a biological system is gained when different types of data (and/or conclusions drawn from the data) are integrated into a larger scale representation or model of the system. Ideally, this type of model is consistent with all available data about the system, and it is then used to generate additional hypotheses to be tested. Computer-based methods intended to formulate models that integrate various events and to test the consistency of these models with respect to the laboratory-based observations on which they are based are potentially very useful. In addition, in contrast to informal models, the consistency of such formal computer-based models with laboratory data can be tested rigorously by methods of formal verification. We combined two formal modeling approaches in computer science that were originally developed for nonbiological system design. One is the interobject approach using the language of live sequence charts (LSCs) with the Play-Engine tool, and the other is the intraobject approach using the language of statecharts and Rhapsody as the tool. Integration is carried out using InterPlay, a simulation engine coordinator. Using these tools, we constructed a combined model comprising three modules. One module represents the early lineage of the somatic gonad of Caenorhabditis elegans in LSCs, whereas a second more detailed module in statecharts represents an interaction between two cells within this lineage that determine their developmental outcome. Using the advantages of the tools, we created a third module representing a set of key experimental data using LSCs. We tested the combined statechart-LSC model by showing that the simulations were consistent with the set of experimental LSCs.- - This small-scale modular example demonstrates the potential for using similar approaches for verification by exhaustive testing of models by LSCs. It also shows the advantages of these approaches for modeling biology.}, author = {Sadot, A. and Fisher, J. and Barak, D. and Admanit, Y. and Stern, M. J. and Hubbard, E. J. A. and Harel, D.}, booktitle = {Computational Biology and Bioinformatics, IEEE/ACM Transactions on}, citeulike-article-id = {2792195}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1371585.1371591}, citeulike-linkout-1 = {http://dx.doi.org/10.1109/TCBB.2007.1076}, citeulike-linkout-2 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4359871}, day = {07}, doi = {10.1109/TCBB.2007.1076}, journal = {Computational Biology and Bioinformatics, IEEE/ACM Transactions on}, keywords = {modeling}, month = {May}, number = {2}, pages = {223--234}, posted-at = {2008-06-10 18:55:11}, priority = {2}, title = {Toward Verified Biological Models}, url = {http://dx.doi.org/10.1109/TCBB.2007.1076}, volume = {5}, year = {2008} }

TY - JOUR ID - citeulike:2792195 L3 - citeulike-article-id:2792195 N2 - The last several decades have witnessed a vast accumulation of biological data and data analysis. Many of these data sets represent only a small fraction of the system's behavior, making the visualization of full system behavior difficult. A more complete understanding of a biological system is gained when different types of data (and/or conclusions drawn from the data) are integrated into a larger scale representation or model of the system. Ideally, this type of model is consistent with all available data about the system, and it is then used to generate additional hypotheses to be tested. Computer-based methods intended to formulate models that integrate various events and to test the consistency of these models with respect to the laboratory-based observations on which they are based are potentially very useful. In addition, in contrast to informal models, the consistency of such formal computer-based models with laboratory data can be tested rigorously by methods of formal verification. We combined two formal modeling approaches in computer science that were originally developed for nonbiological system design. One is the interobject approach using the language of live sequence charts (LSCs) with the Play-Engine tool, and the other is the intraobject approach using the language of statecharts and Rhapsody as the tool. Integration is carried out using InterPlay, a simulation engine coordinator. Using these tools, we constructed a combined model comprising three modules. One module represents the early lineage of the somatic gonad of Caenorhabditis elegans in LSCs, whereas a second more detailed module in statecharts represents an interaction between two cells within this lineage that determine their developmental outcome. Using the advantages of the tools, we created a third module representing a set of key experimental data using LSCs. We tested the combined statechart-LSC model by showing that the simulations were consistent with the set of experimental LSCs.- - This small-scale modular example demonstrates the potential for using similar approaches for verification by exhaustive testing of models by LSCs. It also shows the advantages of these approaches for modeling biology. IS - 2 JF - Computational Biology and Bioinformatics, IEEE/ACM Transactions on EP - 234 TI - Toward Verified Biological Models VL - 5 T2 - Computational Biology and Bioinformatics, IEEE/ACM Transactions on SP - 223 KW - modeling AU - Sadot, A AU - Fisher, J AU - Barak, D AU - Admanit, Y AU - Stern, MJ AU - Hubbard, EJA AU - Harel, D PY - 2008/05/07/ UR - http://dx.doi.org/10.1109/TCBB.2007.1076 ER -