Ordinary differential equations (ODEs) are traditionally used for modeling the continuous behavior within continuous- or hybrid-state feedback control systems. In practice, delay is introduced into the feedback loop if components are spatially or logically distributed. Such delays may significantly alter the system dynamics and unmodeled delays in a control loop consequently have the potential to invalidate any stability and safety certificate obtained on the delay-free model. An appropriate generalization of ODE able to model the delay within the framework of differential equations is delay differential equations (DDEs), as suggested by Bellman and Cooke. Beyond distributed control, DDEs play an important role in the modeling of many processes with time delays, both natural and manmade processes, in biology, physics, economics, engineering, etc. This induces an interest especially in the area of modeling embedded control and formal methods for its verification.

In this work, we focus on automatic safety analysis and verification for continuous systems featuring delays, extending the techniques of safely enclosing set-based initial value problem of ODEs to DDEs. First, as a result of collaborative work, we expose interval-based Taylor over-approximation method to enclose the solution of a simple class of DDE for stability and safety verification. Then, we explore different means of computing safe over- and under-approximations of reachable sets for DDEs by lifting the set-boundary reachability analysis based method of ODEs to a class of DDEs. Furthermore, for the sake of extending the safety properties by involving a number of critical properties such as timing requirements and bounded response rather than just invariance properties, we propose an approach — extending interval-based Taylor over-approximation method for a class of DDEs — to verify arbitrary time-bounded metric interval temporal logic (MITL) formulae, including nesting of modalities.