A Parameterized Formal Model for the Analysis of Preemption-Threshold Scheduling in Real-Time Systems
Time-Critical systems are both complex and critical. Therefore, thorough verification processes of such systems must be performed, including behavior and timing correctness. These systems are usually designed as a set of several interacting tasks and sharing one or more processors. Several schedulin...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2020-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/9027924/ |
| _version_ | 1819132710546833408 |
|---|---|
| author | Imene Ben Hafaiedh Maroua Ben Slimane |
| author_facet | Imene Ben Hafaiedh Maroua Ben Slimane |
| author_sort | Imene Ben Hafaiedh |
| collection | DOAJ |
| description | Time-Critical systems are both complex and critical. Therefore, thorough verification processes of such systems must be performed, including behavior and timing correctness. These systems are usually designed as a set of several interacting tasks and sharing one or more processors. Several scheduling policies have been proposed to manage the dispatch of these tasks for these shared resources so as to respect their predefined deadlines. In this context, preemption threshold scheduling algorithms have been proposed to improve real-time schedulability by managing preemptiveness of tasks. The advantage of these algorithms highly depends on a proper assignment of a set of scheduling attributes, which are priority and preemption threshold. In this paper, we propose a high-level parameterized formal model for the description, analysis and comparison of preemptive, non-preemptive and threshold-based scheduling policies. This model allows to formally verify a set of timing-constraints, in particular schedulability analysis as well as to provide a set of experimental results based on real-time executions. A stochastic version of our model is also proposed allowing to define probabilistic features and to model stochastic real-time tasks, scheduling mechanisms or energy consumption. |
| first_indexed | 2024-12-22T09:35:44Z |
| format | Article |
| id | doaj.art-7a40e25309b74e4e9fae77dc880cbf63 |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-12-22T09:35:44Z |
| publishDate | 2020-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-7a40e25309b74e4e9fae77dc880cbf632022-12-21T18:30:51ZengIEEEIEEE Access2169-35362020-01-018581805819310.1109/ACCESS.2020.29793549027924A Parameterized Formal Model for the Analysis of Preemption-Threshold Scheduling in Real-Time SystemsImene Ben Hafaiedh0https://orcid.org/0000-0001-7941-158XMaroua Ben Slimane1Higher Institute of Informatics (ISI), University of Tunis El Manar (UTM), Tunis, TunisiaNational Engineers School of Tunis (ENIT), University of Tunis EL Manar (UTM), Tunis, TunisiaTime-Critical systems are both complex and critical. Therefore, thorough verification processes of such systems must be performed, including behavior and timing correctness. These systems are usually designed as a set of several interacting tasks and sharing one or more processors. Several scheduling policies have been proposed to manage the dispatch of these tasks for these shared resources so as to respect their predefined deadlines. In this context, preemption threshold scheduling algorithms have been proposed to improve real-time schedulability by managing preemptiveness of tasks. The advantage of these algorithms highly depends on a proper assignment of a set of scheduling attributes, which are priority and preemption threshold. In this paper, we propose a high-level parameterized formal model for the description, analysis and comparison of preemptive, non-preemptive and threshold-based scheduling policies. This model allows to formally verify a set of timing-constraints, in particular schedulability analysis as well as to provide a set of experimental results based on real-time executions. A stochastic version of our model is also proposed allowing to define probabilistic features and to model stochastic real-time tasks, scheduling mechanisms or energy consumption.https://ieeexplore.ieee.org/document/9027924/Formal methodspreemption-threshold schedulingschedulability analysisperformance analysis |
| spellingShingle | Imene Ben Hafaiedh Maroua Ben Slimane A Parameterized Formal Model for the Analysis of Preemption-Threshold Scheduling in Real-Time Systems IEEE Access Formal methods preemption-threshold scheduling schedulability analysis performance analysis |
| title | A Parameterized Formal Model for the Analysis of Preemption-Threshold Scheduling in Real-Time Systems |
| title_full | A Parameterized Formal Model for the Analysis of Preemption-Threshold Scheduling in Real-Time Systems |
| title_fullStr | A Parameterized Formal Model for the Analysis of Preemption-Threshold Scheduling in Real-Time Systems |
| title_full_unstemmed | A Parameterized Formal Model for the Analysis of Preemption-Threshold Scheduling in Real-Time Systems |
| title_short | A Parameterized Formal Model for the Analysis of Preemption-Threshold Scheduling in Real-Time Systems |
| title_sort | parameterized formal model for the analysis of preemption threshold scheduling in real time systems |
| topic | Formal methods preemption-threshold scheduling schedulability analysis performance analysis |
| url | https://ieeexplore.ieee.org/document/9027924/ |
| work_keys_str_mv | AT imenebenhafaiedh aparameterizedformalmodelfortheanalysisofpreemptionthresholdschedulinginrealtimesystems AT marouabenslimane aparameterizedformalmodelfortheanalysisofpreemptionthresholdschedulinginrealtimesystems AT imenebenhafaiedh parameterizedformalmodelfortheanalysisofpreemptionthresholdschedulinginrealtimesystems AT marouabenslimane parameterizedformalmodelfortheanalysisofpreemptionthresholdschedulinginrealtimesystems |