Name
Abstract | ||
|---|---|---|
In this paper, we propose a method for the verification of timed properties for real-time systems featuring a preemptive scheduling 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 automaton, which is a critical parameter for the efficiency of the ensuing verification. Second, the translation is performed by an over-approximating algorithm, which is based on Difference Bound Matrix and therefore efficient, 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 Deadline 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. |
Year | DOI | Venue |
|---|---|---|
2009 | https://doi.org/10.1007/s11241-008-9059-0 | Real-Time Systems |
Keywords | Field | DocType |
Formal methods,Petri nets,Preemptive scheduling,Verification,Hybrid automata | Fixed-priority pre-emptive scheduling,Computer science,Scheduling (computing),Real-time computing,Theoretical computer science,Timed automaton,Rate-monotonic scheduling,Dynamic priority scheduling,Earliest deadline first scheduling,Distributed computing,Formal verification,Hybrid automaton | Journal |
Volume | Issue | ISSN |
41 | 2 | 0922-6443 |
Citations | PageRank | References |
25 | 0.76 | 36 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| didier lime | 1 | 787 | 46.02 |
| olivier h roux | 2 | 671 | 46.30 |