The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - April-June (2008 vol.5)
pp: 223-234
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 non-biological system design. One is the inter-object approach using the language of live sequence charts (LSCs) with the Play-Engine tool, and the other is the intra-object 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 C. elegans in LSCs, while 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.
INDEX TERMS
C. elegans, modeling, statecharts, verification
CITATION
Avital Sadot, Jasmin Fisher, Dan Barak, Yishai Admanit, Michael J. Stern, E. Jane Albert Hubbard, David Harel, "Toward Verified Biological Models", IEEE/ACM Transactions on Computational Biology and Bioinformatics, vol.5, no. 2, pp. 223-234, April-June 2008, doi:10.1109/TCBB.2007.1076
REFERENCES
[1] D. Harel and A. Pnueli, “On the Development of Reactive Systems,” Logics and Models of Concurrent Systems, NATO ASI Series F, K. R. Apt, ed., pp. 477-498, 1985.
[2] D. Harel, “A Grand Challenge for Computing: Full Reactive Modeling of a Multi-Cellular Animal,” Bull. of the EATCS, European Assoc. for Theoretical Computer Science, no. 81, pp. 226-235, 2003.
[3] N. Kam, I.R. Cohen, and D. Harel, “The Immune System as a Reactive System: Modeling T Cell Activation with Statecharts,” Proc. IEEE Symp. Visual Languages and Formal Methods (VLFM '01), part of the IEEE Symp. Human-Centric Computing (HCC '01), pp. 15-22, 2001.
[4] J. Fisher, D. Harel, E.J.A. Hubbard, N. Piterman, M.J. Stern, and N. Swerdlin, “Combining State-Based and Scenario-Based Approaches in Modeling Biological Systems,” Proc. Computational Methods in Systems Biology (CMSB '04), pp. 236-241, 2004.
[5] D. Harel, “A Turing-Like Test for Biological Modeling,” Nature Biotechnology, vol. 23, no. 4, pp. 495-496, Apr. 2005.
[6] E.M. Clarke, O. Grumberg, and D. Peleg, Model Checking. MIT Press, 1999.
[7] L.H. Hartwell, J.J Hopfield, S. Leibler, and A.W. Murray, “From Molecular to Modular Cell Biology,” Nature, vol. 402, no. 6761 Suppl., pp. C47-C52, 1999.
[8] N. Kashtan and U. Alon, “Spontaneous Evolution of Modularity and Network Motifs,” Proc. Nat'l Academy of Sciences, vol. 102, no. 39, pp. 13773-13778, 2005.
[9] P.J. Roy and Q. Morris, “Network News: Functional Modules Revealed during Early Embryogenesis in C. elegans,” Developmental Cell, vol. 9, no. 3, pp. 307-308, 2005.
[10] J.M. Stuart, E. Segal, D. Koller, and S.K. Kim, “A Gene-Coexpression Network for Global Discovery of Conserved Genetic Modules,” Science, vol. 302, no. 5643, pp. 249-255, 2003.
[11] S.Y. Shvartsman, C.B. Muratov, and D.A. Lauffenburger, “Modeling and Computational Analysis of EGF Receptor-Mediated Cell Communication in Drosophila Oogenesis,” Development, vol. 129, no. 11, pp. 2577-2589, 2002.
[12] J. Barjis and I. Barjis, “Formalization of the Protein Production by Means of Petri Nets,” Proc. Int'l Conf. Information Intelligence and Systems (ICIIS '99), 1999.
[13] D.D. Errampalli, C. Priami, and P. Quaglia, “A Formal Language for Computational Systems Biology,” Omics, vol. 8, no. 4, pp. 370-380, 2004.
[14] A. Regev, W. Silverman, and E. Shapiro, “Representation and Simulation of Biochemical Processes Using the Pi-Calculus Process Algebra,” Proc. Pacific Symp. Biocomputing, vol. 6, pp.459-470, 2001.
[15] C. Talcott and D.L. Dill, “The Pathway Logic Assistant,” Proc. Computational Methods in Systems Biology (CMSB '05), pp. 228-239, 2005.
[16] M. Calder, V. Vyshemirsky, D. Gilbert, and R. Orton, “Analysis of Signaling Pathways Using the PRISM Model Checker,” Proc. Computational Methods in Systems Biology (CMSB '05), pp. 179-190, 2005.
[17] L. Calzone, F. Fages, and S. Soliman, “BIOCHAM: An Environment for Modeling Biological Systems and Formalizing Experimental Knowledge,” Bioinformatics, vol. 22, no. 14, pp. 1805-1807, 2006.
[18] R. Ghosh, A. Tiwari, and C. Tomlin, “Automated Symbolic Reachability Analysis with Application to Delta-Notch Signaling Automata,” Proc. Hybrid Systems: Computation and Control (HSCC '03), pp. 233-248, 2003.
[19] R. Alur, C. Belta, F. Ivancic, V. Kumar, M. Mintz, G. Pappas, H. Rubin, and J. Schug, “Hybrid Modeling and Simulation of Biomolecular Networks,” Proc. Hybrid Systems: Computation and Control (HSCC '01), pp. 19-32, 2001.
[20] S. Efroni, D. Harel, and I.R. Cohen, “Toward Rigorous Comprehension of Biological Complexity: Modeling, Execution, and Visualization of Thymic T-Cell Maturation,” Genome Research, vol. 13, no. 11, pp. 2485-2497, 2003.
[21] J. Fisher, N. Piterman, E.J.A. Hubbard, M.J. Stern, and D. Harel, “Computational Insights into Caenorhabditis elegans Vulval Development,” Proc. Nat'l Academy of Sciences, vol. 102, no. 6, pp. 1951-1956, 2005.
[22] D. Harel, S. Efroni, and I.R. Cohen, “Reactive Animation,” Proc. First Int'l Symp. Formal Methods for Components and Objects (FMCO '02) , invited paper, pp. 136-153, 2003.
[23] N. Kam, D. Harel, H. Kugler, R. Marelly, A. Pnueli, E.J.A. Hubbard, and M.J. Stern, “Formal Modeling of C. elegans Development: A Scenario-Based Approach,” Proc. First Int'l Workshop Computational Methods in Systems Biology (ICMSB '03), pp. 4-20, Feb. 2003.
[24] D. Barak, D. Harel, and R. Marelly, “InterPlay: Horizontal Scale-Up and Transition to Design in Scenario-Based Programming,” IEEE Trans. Software Eng., vol. 32, no. 7, pp. 467-485, 2006, earlier version in Lectures on Concurrency and Petri Nets, pp.66-86, Springer, 2004.
[25] J. Kimble and D. Hirsh, “The Postembryonic Cell Lineages of the Hermaphrodite and Male Gonads in Caenorhabditis elegans,” Developmental Biology, vol. 70, no. 2, pp. 396-417, 1979.
[26] J.E. Kimble and J.G. White, “On the Control of Germ Cell Development in Caenorhabditis elegans,” Developmental Biology, vol. 81, no. 2, pp. 208-219, 1981.
[27] I.S. Greenwald, P.W. Sternberg, and H.R. Horvitz, “The lin-12 Locus Specifies Cell Fates in Caenorhabditis elegans,” Cell, vol. 34, no. 2, pp. 435-444, 1983.
[28] S.T. Henderson, D. Gao, E.J. Lambie, and J. Kimble, “lag-2 May Encode a Signaling Ligand for the GLP-1 and LIN-12 Receptors of C. elegans,” Development, vol. 120, no. 10, pp. 2913-2924, 1994.
[29] E.J. Lambie and J. Kimble, “Two Homologous Regulatory Genes, lin-12 and glp-1, Have Overlapping Functions,” Development, vol. 112, no. 1, pp. 231-240, 1991.
[30] F.E. Tax, J.J. Yeargers, and J.H. Thomas, “Sequence of C. elegans lag-2 Reveals a Cell-Signaling Domain Shared with Delta and Serrate of Drosophila,” Nature, vol. 368, no. 6467, pp. 150-154, 1994.
[31] J. Yochem, K. Weston, and I. Greenwald, “The Caenorhabditis elegans lin-12 Gene Encodes a Trans-Membrane Protein with Overall Similarity to Drosophila Notch,” Nature, vol. 335, no. 6190, pp. 547-550, 1988.
[32] G. Seydoux and I. Greenwald, “Cell Autonomy of lin-12 Function in a Cell Fate Decision in C. elegans,” Cell, vol. 57, no. 7, pp. 1237-1245, 1989.
[33] H.A. Wilkinson, K. Fitzgerald, and I. Greenwald, “Reciprocal Changes in Expression of the Receptor lin-12 and Its Ligand lag-2 Prior to Commitment in a C. elegans Cell Fate Decision,” Cell, vol. 79, no. 7, pp. 1187-1198, 1994.
[34] X. Karp and I. Greenwald, “Post-Transcriptional Regulation of the E/Daughterless Ortholog HLH-2, Negative Feedback, and Birth Order Bias during the AC/VU Decision in C. elegans,” Genes and Development, vol. 17, no. 24, pp. 3100-3111, 2003.
[35] J.R. Collier, N.A. Monk, P.K. Maini, and J.H. Lewis, “Pattern Formation by Lateral Inhibition with Feedback: A Mathematical Model of Delta-Notch Intercellular Signaling,” J. Theoretical Biology, vol. 183, no. 4, pp. 429-446, 1996.
[36] G. Marnellos, G.A. Deblandre, E. Mjolsness, and C. Kintner, “Delta-Notch Lateral Inhibitory Patterning in the Emergence of Ciliated Cells in Xenopus: Experimental Observations and a Gene Network Model,” Proc. Pacific Symp. Biocomputing, vol. 5, pp. 329-340, 2000.
[37] H. Matsuno, R. Murakami, R. Yamane, N. Yamasaki, S. Fujita, H. Yoshimori, and S. Miyano, “Boundary Formation by Notch Signaling in Drosophila Multicellular Systems: Experimental Observations and Gene Network Modeling by Genomic Object Net,” Proc. Pacific Symp. Biocomputing, pp. 152-163, 2003.
[38] D. Harel, “Statecharts: A Visual Formalism for Complex Systems,” Science of Computer Programming, vol. 8, pp. 231-274, 1987.
[39] D. Harel and E. Gery, “Executable Object Modeling with Statecharts,” Computer, vol. 30, no. 7, pp. 31-42, July 1997.
[40] W. Damm and D. Harel, “LSCs: Breathing Life into Message Sequence Carts,” Formal Methods in System Design, vol. 19, no. 1, pp. 45-80, 2001.
[41] D. Harel and R. Marelly, Come, Let's Play—Scenario-Based Programming Using LSCs and the Play-Engine. Springer, 2003.
[42] H.R. Horvitz and I. Herskowitz, “Mechanisms of Asymmetric Cell Division: Two Bs or Not Two Bs, That Is the Question,” Cell, vol. 68, no. 2, pp. 237-255, 1992.
[43] L.A. Segal, Mathematical Models in Molecular and Cellular Biology. Cambridge Univ. Press, 1980.
[44] J. Kimble, “Alterations in Cell Lineage Following Laser Ablation of Cells in the Somatic Gonad of Caenorhabditis elegans,” Developmental Biology, vol. 87, no. 2, pp. 286-300, 1981.
[45] I. Greenwald, “LIN-12/Notch Signaling: Lessons from Worms and Flies,” Genes and Development, vol. 12, no. 12, pp. 1751-1762, 1998.
[46] N.A. Lynch, Distributed Algorithms. Morgan Kaufmann, 1996.
[47] N. Kam, “The Immune System As A Reactive System: Modeling T-Cell Activation Using Statecharts,” master's thesis, Weizmann Inst. of Science, 2000.
[48] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
17 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool