Formal modeling for a real-time scheduler and schedulability analysis

Sung Jae Kim, Jin Young Choi

Research output: Chapter in Book/Report/Conference proceedingChapter

1 Citation (Scopus)

Abstract

The reliability of safety-critical embedded real-time system depends partly on that of the system design. Because of this, formal methods have been adopted in the design phase of developing such systems, and various kinds of formal methods have been introduced and used in practice. Many successful results have been published in application systems/softwares. However, studies on formal specification for embedded kernel, like scheduler, are relatively few due to the complexity of the software. In this paper, we present a formal specification for real-time scheduler based on SyncCharts. We specify a scheduler of which policies are rate monotonic, as well as Priority Ceiling Protocol, and perform schedulability analysis by formal verification. Once requirements of the real-time scheduler and timing properties of given tasks are satisfied, a real code can be automatically generated and, we believe, ported in a real target platform.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsVictor Malyshkin
PublisherSpringer Verlag
Pages253-258
Number of pages6
ISBN (Print)3540406735
DOIs
Publication statusPublished - 2003

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2763
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Formal modeling for a real-time scheduler and schedulability analysis'. Together they form a unique fingerprint.

  • Cite this

    Kim, S. J., & Choi, J. Y. (2003). Formal modeling for a real-time scheduler and schedulability analysis. In V. Malyshkin (Ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 253-258). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2763). Springer Verlag. https://doi.org/10.1007/978-3-540-45145-7_23