Model Checking Tasking Sets using Time Petri Nets and Uppaal
| Title | Model Checking Tasking Sets using Time Petri Nets and Uppaal |
| Publication Type | Conference Paper |
| Year of Publication | 2004 |
| Authors | Furfaro, A, Nigro, L, Pupo, F |
| Conference Name | Proc. of 28th IFAC/IFIP Workshop on Real-Time Programming (WRTP'04) |
| Date Published | September, 6–8 |
| Conference Location | Istanbul, Turkey |
| Abstract | This paper proposes a mapping of Time Petri Nets augmented with pre-emptable transitions (PTPN’s) to UPPAAL which allows schedulability analysis through model checking of task sets. A template for PTPN transition was developed which is used in combination with a clock suspension/resume mechanism and discrete time. The technique proves useful for the verification of pre-emptive tasking sets under mutual exclusion, priorities and pre-emptable resources (processors). The achieved mechanism is demonstrated by some examples. |