Modelling and Schedulability Analysis of Real-time Sequence Patterns using Time Petri Nets and Uppaal
|Title||Modelling and Schedulability Analysis of Real-time Sequence Patterns using Time Petri Nets and Uppaal|
|Publication Type||Conference Paper|
|Year of Publication||2007|
|Authors||Furfaro, A, Nigro, L|
|Conference Name||Proc. of International Workshop on Real Time Software (RTS'07)|
|Date Published||October 16|
This paper proposes an original approach to the schedulability analysis of real-time systems specified by Time Petri Nets (TPNs). The focus is on sequence patterns of transition firings (execution tasks). A TPN model is first translated in the Timed Automata terms of the popular Uppaal tool. Then schedulability properties of tasks are verified through reachability analysis. The approach is efficient and scalable. The paper demonstrates the concrete application of the approach through examples. Finally, conclusions are drawn together with an indication of on-going and future work.