  Automated verification of living organism models allows us to gain previously
unknown knowledge about underlying biological processes. In this paper, we show
the benefits to use parametric time Petri nets in order to analyze precisely
the dynamic behavior of biological oscillatory systems. In particular, we focus
on the resilience properties of such systems. This notion is crucial to
understand the behavior of biological systems (e.g. the mammalian circadian
rhythm) that are reactive and adaptive enough to endorse major changes in their
environment (e.g. jet-lags, day-night alternating work-time). We formalize
these properties through parametric TCTL and demonstrate how changes of the
environmental conditions can be tackled to guarantee the resilience of living
organisms. In particular, we are able to discuss the influence of various
perturbations, e.g. artificial jet-lag or components knock-out, with regard to
quantitative delays. This analysis is crucial when it comes to model
elicitation for dynamic biological systems. We demonstrate the applicability of
this technique using a simplified model of circadian clock.
