Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking

Nan Guan, Zonghua Gu, Qingxu Deng, Shuaihong Gao, Ge Yu

Research output: Chapter in book / Conference proceedingConference article published in proceeding or bookAcademic researchpeer-review

52 Citations (Scopus)

Abstract

To determine schedulability of priority-driven periodic tasksets on multi-processor systems, it is necessary to rely on utilization bound tests that are safe but pessimistic, since there is no known method for exact schedulability analysis for multi-processor systems analogous to the response time analysis algorithm for single-processor systems. In this paper, we use model-checking to provide a technique for exact multiprocessor scheduability analysis by modeling the real-time multi-tasking system with Timed Automata (TA), and transforming the schedulability analysis problem into the reachability checking problem of the TA model.
Original languageEnglish
Title of host publicationSoftware Technologies for Embedded and Ubiquitous Systems - 5th IFIP WG 10.2 International Workshop, SEUS 2007, Revised Papers
Pages263-272
Number of pages10
Publication statusPublished - 1 Dec 2007
Externally publishedYes
Event5th IFIP WG 10.2 International Workshop on Software Technologies for Embedded and Ubiquitous Systems, SEUS 2007 - Santorini Island, Greece
Duration: 7 May 20078 May 2007

Publication series

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

Conference

Conference5th IFIP WG 10.2 International Workshop on Software Technologies for Embedded and Ubiquitous Systems, SEUS 2007
Country/TerritoryGreece
CitySantorini Island
Period7/05/078/05/07

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking'. Together they form a unique fingerprint.

Cite this