Handling Delay Differential Equations in Automatic Verification

17. August 2017, 16:00 , 17:30

Veranstalter:  Peter Nazier Mosaad, Universität Oldenburg
Ort:  OFFIS, Escherweg 2, Raum F02

Abstract:
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 so-
lution 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 reach-
ability 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-ap-
proximation method for a class of DDEs— to verify arbitrary time-bounded metric interval temporal logic
(MITL) formulae, including nesting of modalities.
Betreuer: Prof. Dr. Martin Fränzle