RNTI

MODULAD
Verification of embbeded systems with preemption: a negative result
In ISoLA 2007, vol. RNTI-SM-1, pp.97-108
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.