Title :
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
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;
Conference_Titel :
Design Automation Conference, 2007. DAC '07. 44th ACM/IEEE
Conference_Location :
San Diego, CA
Print_ISBN :
978-1-59593-627-1