Formal verification of real-time systems with preemptive scheduling

Abstract. In this paper, we propose a method for the verification of timed properties for real-time systems featuring a preemptive schedul-ing policy: the system, modeled as a scheduling time Petri net, is first translated into a linear hybrid automaton to which it is time-bisimilar. Timed properties can then be verified using HyTech. The efficiency of this approach leans on two major points: first, the translation features a minimization of the number of variables (clocks) of the resulting automa-ton, which is a critical parameter for the efficiency of the ensuing veri-fication. Second, the translation is performed by an over-approximating algorithm, which is based on Difference Bound Matrix and therefore effi-cient, that nonetheless produces a time-bisimilar automaton despite the over-approximation. The proposed modeling and verification method are generic enough to account for many scheduling policies. In this paper, we specifically show how to deal with Fixed Priority and Earliest Dead-line First policies, with the possibility of using Round-Robin for tasks with the same priority. We have implemented the method and give some experimental results illustrating its efficiency.