Optimization of Static Task and Bus Access Schedules for Time-Triggered Distributed Embedded Systems with Model-Checking

Author

Gu, Zonghua ; He, Xiuqiang ; Yuan, Mingxuan

Author_Institution

Hong Kong Univ. of Sci. & Technol., Kowloon

fYear

2007

fDate

4-8 June 2007

Firstpage

294

Lastpage

299

Abstract

Time-triggered protocol for the bus and static task scheduling for the CPU are widely used in safety-critical distributed embedded systems. Researchers have presented efficient heuristic algorithms to jointly optimize static task and bus access schedules. In this paper, we use the model checker SPIN to provide a flexible and configurable technique for obtaining provably optimal solutions, and evaluate its performance tradeoffs compared to heuristic algorithms.

Keywords

embedded systems; program verification; safety-critical software; scheduling; system buses; CPU; SPIN; bus access schedule; distributed embedded system; model-checking; safety-critical embedded system; static task schedule; time-triggered embedded system; time-triggered protocol; Access protocols; Embedded system; Helium; Heuristic algorithms; Operating systems; Permission; Processor scheduling; Runtime; Scheduling algorithm; Time division multiple access; Algorithms; Performance; Verification; model-checking; optimization; scheduling;

fLanguage

English

Publisher

ieee

Conference_Titel

Design Automation Conference, 2007. DAC '07. 44th ACM/IEEE

Conference_Location

San Diego, CA

ISSN

0738-100X

Print_ISBN

978-1-59593-627-1

Type

conf

Filename

4261194