Vlad Rusu. Verifying periodic task-control systems. In International workshop on Hybrid and Real-Time Systems (HART'97), Grenoble (France), pp 63-69, 1997, LNCS 1201.

Abstract

This paper deals with the automated verification of a class of task-control programs with periods, durations, and scheduling specifications. Such systems are translated into Periodic Hybrid Automata for verification. We show that safety, liveness, and time-bounded properties are decidable for the considered systems.

Full postscript text.