Formal modeling for a real-time scheduler and schedulability analysis

Sung Jae Kim, Jin Young Choi

    Research output: Chapter in Book/Report/Conference proceedingChapter

    2 Citations (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
    • General Computer Science

    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