mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Modelling, Verification and Synthesis of Two-Tier Hierarchical Fixed-Priority Preemptive Scheduling
Mälardalen University, School of Innovation, Design and Engineering.ORCID iD: 0000-0001-6157-5199
Mälardalen University, School of Innovation, Design and Engineering.ORCID iD: 0000-0003-4040-3480
Mälardalen University, School of Innovation, Design and Engineering.ORCID iD: 0000-0001-6132-7945
2011 (English)In: Proceedings - 23rd EUROMICRO Conference on Real-Time Systems (ECRTS'11), 2011, 172-181 p.Conference paper, Published paper (Refereed)
Abstract [en]

Hierarchical scheduling has major benefits when it comes to integrating hard real-time applications. One of those benefits is that it gives a clear runtime separation of applications in the time domain. This in turn gives a protection against timing error propagation in between applications. However, these benefits rely on the assumption that the scheduler itself schedules applications correctly according to the scheduling parameters and the chosen scheduling policy. A faulty scheduler can affect all applications in a negative way. Hence, being able to guarantee that the scheduler is correct is of great importance. Therefore, in this paper, we study how properties of hierarchical scheduling can be verified. We model a hierarchically scheduled system using task automata, and we conduct verification with model checking using the Times tool. Further, we generate C-code from the model and we execute the hierarchical scheduler in the Vx Works kernel. The CPU and memory overhead of the modelled scheduler is compared against an equivalent manually coded two-level hierarchical scheduler. We show that the worst-case memory consumption is similar and that there is a considerable difference in CPU overhead.

Place, publisher, year, edition, pages
2011. 172-181 p.
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-13734DOI: 10.1109/ECRTS.2011.24ISI: 000323257300016Scopus ID: 2-s2.0-80052990420ISBN: 9780769544427 (print)OAI: oai:DiVA.org:mdh-13734DiVA: diva2:466280
Conference
23rd Euromicro Conference on Real-Time Systems, ECRTS 2011;Porto;5 July 2011 through 8 July 2011
Available from: 2011-12-15 Created: 2011-12-15 Last updated: 2014-01-07Bibliographically approved
In thesis
1. On the Development of Hierarchical Real-Time Systems
Open this publication in new window or tab >>On the Development of Hierarchical Real-Time Systems
2012 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Hierarchical scheduling (also referred to as resource reservation) is a hot topic within the research of real-time systems. It has many advantages such that it can facilitate software integration, fault isolation, structured analysis, legacy system integration etc. The main idea is to partition resources into well defined slots and the resource itself may be the processor, memory etc. This technique is rarely used in real-time applications, however, it is well adopted in the avionics industry in order to isolate error propagation between system parts, and facilitate analysis of the system.Much of the research within resource reservation deals with theoretical schedulability analysis of partitioned systems, including shared resources (other than the processor). We will in this thesis address more practical issues related to resource reservation. We focus on implementation and prototyping aspects, as well as verification and instrumentation. One of our assumptions is that we deal only with fixed-priority preemptive scheduling (FPPS).The first part in this thesis deals with individual software systems that may have its own tasks as well as a scheduler and it is assumed to be part of another larger system, hence, we refer to this individual system as a subsystem. The subsystem is assumed to be integrated together with other subsystems, but at a early stage, we make it possible to simulate the subsystem running together with the rest of the subsystems. This "simulation`` does not require the actual resource reservation mechanism, the only requirement is an operating system with support for FPPS. This pre-study may be a natural step towards the "real`` integration, since each individual subsystem can be test executed within its assigned partition. All subsystems are assumed to run together using a resource reservation mechanism (during the actual integration). We have developed two prototypes of this mechanism. The first prototype is hand-crafted and it is equipped with a program tracer for partitoned based schedulers. This instrumentation is useful for debugging and visualization of program traces for this type of scheduling. The second prototype is developed using timed automata with tasks (task automata). This model-based scheduler is verified for correctness and it is possible to automatically generate source code for the scheduler. We have successfully synthesized this scheduler for the real-time operating system VxWorks. However, it can easily be executed on most other platforms. Both prototypes has pros and cons. The first version has good performance while the second can guarantee its correctness, hence, there is a trade-off between performance and correctness.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2012. 154 p.
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 155
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-14633 (URN)987-91-7485-075-8 (ISBN)
Presentation
2012-06-12, Kappa, Högskoleplan 1, Västerås, 10:15 (English)
Opponent
Supervisors
Available from: 2012-05-21 Created: 2012-05-21 Last updated: 2013-12-03Bibliographically approved
2. Synthesis and Synchronization Support for Hierarchically Scheduled Real-Time Systems
Open this publication in new window or tab >>Synthesis and Synchronization Support for Hierarchically Scheduled Real-Time Systems
2014 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

A piece of software, that we define as a software system, can consist of anything from a few lines of program code or the entire software stack in a vehicle. Software systems can be divided into smaller and partially independent parts called subsystems/partitions (we use the words partition and subsystem interchangeably). The non-functional isolation of subsystems, that appears when the software system is hierarchically divided, has great advantages when it comes to preventing fault propagation between subsystems. The hierarchical division, that we refer to as hierarchical scheduling, has other advantages as well. It facilitates re-usability and it makes timing analysis of software systems easier. Hierarchical scheduling has been shown to be a useful tool in counteracting the verification challenges that comes from the growing complexity in software. For example, the avionics-specification ARINC653 and the safety-critical operating systems seL4 and PikeOS safely divide resources for independent safety-critical applications by using hierarchical scheduling.

Hierarchical scheduling can be implemented in many different ways, depending on what resource that is supposed to be shared among applications. The resource could be the CPU, memory, network etc. The work in this thesis is focused on the practical aspects of timing isolation among subsystems, i.e., sharing of the CPU resource. Hence, this work elaborates on how to adapt and extend the operating-system task-scheduler to support hierarchical scheduling. We have focused on both independent and semi-dependent subsystems. Independent subsystems only share general resources such as the CPU and memory. Semi-independent subsystems share not only the general resources, but also other logical resources that can only be accessed in a mutually exclusive way, i.e., by one subsystem at a time. An example of such a resource could be a shared memory-space, e.g., a database, a memory-mapped device etc.

This thesis has two main parts related to hierarchical scheduling: scheduler synthesis, and synchronization.

Scheduler synthesis is related to implementation and design strategies when adding support for hierarchical scheduling in an operating system. We have focused on various operating systems that were lacking the feature of hierarchical scheduling. The two most interesting operating systems that we worked on was Linux and seL4. These two operating systems represent two extremes, where Linux is more focused towards soft real-time systems and seL4 towards pure hard real-time (safety-critical) systems. Linux-based systems have in general less strict demands on correctness and more requirements on usability. Usability implies less installation efforts and less limitations in the usage of the available Linux functionality. The usability aspect is especially important for Linux systems since kernel updates occur much more frequently compared to any other operating system. Hence, extending/modifying the functionality of Linux must be done in a way that does not require any modifications to the kernel. seL4 on the other hand has strict requirements on safety, i.e., functional and non-functional correctness, but also performance efficiency. Guaranteeing correctness implies a potential loss of performance due to the added overhead that the verified software can bring. The correctness aspect includes strategies on how to verify hierarchical schedulers, but also how to minimize the scheduler overhead and achieve as good run-time performance as possible. Conclusively, there are many challenges when it comes to scheduler synthesis. There are requirements on performance, usability, correctness etc. The contribution in the synthesis part includes a scheduler framework called ExSched (External Scheduler). We have also contributed with a novel approach to verify hierarchical schedulers, and a code generator called TAtoC (Timed Automata to C) which contributes to the effective run-time performance of synthesized timed-automata models.

The second part of this thesis, synchronization, is an important general aspect of hierarchically scheduled systems since the isolation of subsystems makes resource sharing among subsystems more challenging. We have advanced the state-of-the-art in this research area by introducing a new synchronization protocol called RRP (Rollback Resource Policy) that improves on the robustness and run-time performance compared to the existing protocols. We have also conducted a large scale experimental evaluation of all existing protocols that we have implemented in the widely used real-time operating system VxWorks.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2014. 266 p.
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 149
National Category
Computer Engineering
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-23462 (URN)978-91-7485-131-1 (ISBN)
Public defence
2014-01-31, Gamma, Västerås, 10:00 (English)
Opponent
Supervisors
Available from: 2014-01-07 Created: 2013-12-12 Last updated: 2014-01-21Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Åsberg, MikaelPettersson, PaulNolte, Thomas
By organisation
School of Innovation, Design and Engineering
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 89 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf