On the verification by approximation of duration systems

Abstract EN

We consider the problem of verifying invariance properties for duration systems.

Such systems are (extended) timed graphs with duration variables.

They are especially suitable for describing real time schedulers.

However, for this kind of systems, the verification problem of invariance properties is in general undecidable.

We propose an over approximation method based on a particular extension of a given duration system, and we show that our over approximation includes all the digitization of all the real computations of the duration system.

The over-approximated system can then be used to perform an interesting close analysis of invariance properties of the initial system, while other existing approaches fail.