Verification of embbeded systems with preemption: a negative result
Résumé
The aim of this article is to explore the problem of verification of
preemptive communicating timed processes, i.e., timed processes which can be
suspended and resumed by an on-line scheduler. The contribution of the article
is to show that this problem is unfortunately undecidable. We discuss then an
alternative verification method to overcome this negative result.