2016 IEEE International High Level Design Validation and Test Workshop (HLDVT) (2016)
Santa Cruz, CA, USA
Oct. 7, 2016 to Oct. 8, 2016
Natasa Miskov-Zivanov , University of Pittsburgh, Electrical and Computer Engineering, Bioengineering Computational and Systems Biology, Pittsburgh, PA, USA
Paolo Zuliani , Newcastle University, Computer Science, Newcastle upon Tyne, UK
Qinsi Wang , Carnegie Mellon University, Computer Science, Pittsburgh, PA, USA
Edmund M. Clarke , Carnegie Mellon University, Computer Science, Pittsburgh, PA, USA
James R. Faeder , University of Pittsburgh, Computational and Systems Biology, Pittsburgh, PA, USA
We use computational modeling and formal analysis techniques to study temporal behavior of a discrete logical model of the na´ve T cell differentiation. The model is analyzed formally and automatically by performing temporal logic queries via statistical model checking. While the model can be verified and then further explored using Monte Carlo simulations, model checking allows for much more efficient analysis by testing a large set of system properties, with much smaller runtime than the one required by simulations. The results obtained using model checking provide details about relative timing of events in the system, which would otherwise be very cumbersome and time consuming to obtain through simulations only. We efficiently test a large number of properties, and confirm or reject hypotheses that were drawn from previous analysis of experimental and simulation data.
Model checking, Analytical models, Computational modeling, Trajectory, Data models, Steady-state, Numerical models
N. Miskov-Zivanov, P. Zuliani, Q. Wang, E. M. Clarke and J. R. Faeder, "High-level modeling and verification of cellular signaling," 2016 IEEE International High Level Design Validation and Test Workshop (HLDVT), Santa Cruz, CA, USA, 2016, pp. 162-169.