Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Real-time task schedulability analysis via spotlight abstraction
Thesis (PhD (Computer Science))--University of Pretoria, 2023.
Saved in:
| Other Authors: | |
|---|---|
| Format: | Thesis |
| Language: | English |
| Published: |
University of Pretoria
2024
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613546254172160 |
|---|---|
| access_status_str | Open Access |
| author2 | Gruner, Stefan |
| author_browse | Gruner, Stefan |
| author_facet | Gruner, Stefan |
| collection | Thesis |
| dc_rights_str_mv | © 2023 University of Pretoria. All rights reserved. The copyright in this work vests in the University of Pretoria. No part of this work may be reproduced or transmitted in any form or by any means, without the prior written permission of the University of Pretoria. |
| description | Thesis (PhD (Computer Science))--University of Pretoria, 2023. |
| format | Thesis |
| id | oai:repository.up.ac.za:2263/98004 |
| institution | University of Pretoria (South Africa) |
| language | English |
| last_indexed | 2026-06-10T12:37:51.914Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from UPSpace — University of Pretoria Institutional Repository |
| publishDate | 2024 |
| publishDateRange | 2024 |
| publishDateSort | 2024 |
| publisher | University of Pretoria |
| publisherStr | University of Pretoria |
| record_format | dspace |
| source_str | UPSpace — University of Pretoria Institutional Repository |
| spelling | oai:repository.up.ac.za:2263/98004 Real-time task schedulability analysis via spotlight abstraction Gruner, Stefan u12238156@tuks.co.za Timm, Nils Nxumalo, Madoda Timed Automata Model Checking Schedulability Analyisis Spotlight Abstraction Real-time Systems UCTD Thesis (PhD (Computer Science))--University of Pretoria, 2023. The schedulability analysis of real-time systems is challenged by the state space complexity of such systems. It is difficult to develop concrete state space models that can be used to verify the schedulability of real-time systems. This thesis solves the state space complexity problem by means of a new abstraction technique that enables an automated and efficient verification of schedulability properties of real-time task sets. The technique is applied to task queues under the {FIFO and EDF scheduling policies. The approach is based on the spotlight abstraction principle. The novel spotlight abstraction approach partitions the scheduler task queue into a `spotlight' and a `shade'. A small number of tasks that appear to a specified depth at the front of the queue and will be executed in the near future are placed in the spotlight. The shade contains the remaining tasks at the back of the queue which is executed only after the spotlight tasks have been processed. A timed automaton is generated from the spotlight to form an abstract model of the concrete system. The schedulability analysis of the spotlight is performed whereby the behaviour of the shade is summarised and the partial schedulability result for the spotlight tasks is saved for later re-use in the subsequent iterations. In each iteration, if the result is still inconclusive and there still exist tasks in the shade, more tasks are brought from the shade into the spotlight, with which the model checker can proceed. The iterations are continued until a decisive schedulability result (yes or no) is obtained. A new tool, called TVMC, that implements the spotlight abstraction-based model checking approach has been developed. An experimental performance evaluation of the abstraction-based TVMC against model checking without abstraction is presented. Empirical results showed that the execution times of the abstraction-based TVMC were faster than the ones of the approach without abstraction. Moreover, the spotlight abstraction TVMC handled larger task sets whereas the non-abstraction case failed to verify task sets with sizes greater than six due to state explosion. This work also presents an experimental comparison of TVMC against established tools: Timestool and the Uppaal platform based RTLib. TVMC was able to cope with the state explosion problem considerably better than Timestool and RTLib since it was able to handle significantly larger task sets and to finish the analysis in a similar amount of run-times. Computer Science PhD (Computer Science) Unrestricted Faculty of Engineering, Built Environment and Information Technology 2024-09-04T06:14:57Z 2024-09-04T06:14:57Z 2024-09-02 2023-12-08 Thesis * S2024 http://hdl.handle.net/2263/98004 10.25403/UPresearchdata.26799829 en © 2023 University of Pretoria. All rights reserved. The copyright in this work vests in the University of Pretoria. No part of this work may be reproduced or transmitted in any form or by any means, without the prior written permission of the University of Pretoria. application/pdf University of Pretoria |
| spellingShingle | Timed Automata Model Checking Schedulability Analyisis Spotlight Abstraction Real-time Systems UCTD Real-time task schedulability analysis via spotlight abstraction |
| title | Real-time task schedulability analysis via spotlight abstraction |
| title_full | Real-time task schedulability analysis via spotlight abstraction |
| title_fullStr | Real-time task schedulability analysis via spotlight abstraction |
| title_full_unstemmed | Real-time task schedulability analysis via spotlight abstraction |
| title_short | Real-time task schedulability analysis via spotlight abstraction |
| title_sort | real time task schedulability analysis via spotlight abstraction |
| topic | Timed Automata Model Checking Schedulability Analyisis Spotlight Abstraction Real-time Systems UCTD |
| url | http://hdl.handle.net/2263/98004 |