文献

J-GLOBAL ID：201702233469426566   整理番号：17A0777175

オーバロードリアルタイムシステムのためのSMTベースのスケジューリング

SMT-Based Scheduling for Overloaded Real-Time Systems

著者 (4件)： CHENG Zhuo (School of Information Science, Japan Advanced Institute of Science and Technology) ,  ZHANG Haitao (School of Information Science and Engineering, Lanzhou University) ,  TAN Yasuo (School of Information Science, Japan Advanced Institute of Science and Technology) ,  LIM Yuto (School of Information Science, Japan Advanced Institute of Science and Technology)
資料名： IEICE Transactions on Information and Systems (Web)  (IEICE Transactions on Information and Systems (Web))
巻： E100.D  号： 5  ページ： 1055-1066(J-STAGE)  発行年： 2017年 
JST資料番号： U0469A  ISSN： 1745-1361  資料種別： 逐次刊行物 (A)
記事区分： 短報  発行国： 日本 (JPN)  言語： 英語 (EN)

抄録/ポイント： リアルタイムシステムでは,タスクを期限前に完了することを必要とした。通常の作業負荷の状態では,適切なスケジューリング方策を持つスケジューラはすべてのタスクを期限に対処することができた。しかし,実際の環境では,システムの負荷が大きく異なる場合があった。システム作業負荷が重くなりすぎると,すべてのタスクが期限に合わせることができる実行可能なスケジュールが存在しないために,システムが過負荷になり,いくつかのタスクが期限を逸してしまうことがあった。締め切りに間に合わなかったタスクに起因するシステム性能の低下の程度を緩和するために,スケジューリングの設計が重要であった。多くの設計目標を考慮することができた。本稿では,まず,締め切りまでに完了できるタスクの総数を最大にすることに焦点を当てた。充足可能性モジュロ理論(SMT)に基づくスケジューリング手法を提案した。この方法では,スケジューリングの問題を充足可能性の問題として扱った。重要な作業は,一次言語を使用して充足可能性問題を正式化することであった。定式化の後,この充足可能性問題を解決するために,SMTソルバ(例えば,Z3,Yices)を採用した。最適なスケジュールを,SMTソルバから返された解モデルに基づいて生成した。この方法の正確さと生成したスケジュールの最適性を,簡単な方法で確認することができた。提案手法の時間効率を様々なシミュレーションにより実証した。さらに,提案したSMTベースのスケジューリング方法では,著者らはスケジューリング制約をシステム制約およびターゲット制約として定義した。つまり,著者らが他のターゲットを実現するためにスケジューリングを設計したい場合は,ターゲット制約のみを変更する必要があった。この利点を実証するために,著者らは,SMTベースのスケジューリング手法を他の設計ターゲット,すなわち有効なプロセッサ利用の最大化と完成したタスクの取得値の最大化に適用した。非常に小さい変化だけを,適応手順に必要としたが,提案したSMTベースのスケジューリング方法は柔軟で十分に一般的であるということを意味した。(翻訳著者抄録)

シソーラス用語： *可能性 ,  *スケジューリング ,  過負荷 ,  実時間処理 ,  オペレーティングシステム ,  応用プログラム ,  言語 ,  制約条件 ,  作業負荷
準シソーラス用語： *充足可能性 ,  オーバロード ,  リアルタイムシステム ,  スケジューラ ,  ソルバ ,  制約

著者キーワード (4件)： real-time scheduling ,  SMT ,  overload ,  satisfiability problem

分類 (2件)： 工程管理  (KB03030P) ,  その他の情報処理  (JE15050M)

引用文献 (23件)：

• [1] Z. Cheng, H. Zhang, Y. Tan, and Y. Lim, “Scheduling overload for real-time systems using SMT solver,” Proc. 17th IEEE/ACIS Int. Conf. on Software Eng., Artificial Intell., Networking and Parallel/Distributed Computing, Shanghai, China, pp.189-194, May30 -June 1, 2016.
• [2] F. Zhang and A. Burns, “Schedulability analysis for real-time systems with EDF scheduling,” IEEE Trans. Comput., vol.58, no.9, pp.1250-1258, April 2009.
• [3] S.K. Baruah, J. Haritsa, and N. Sharma, “On-line scheduling to maximize task completions,” Proc. 15th IEEE Real-Time Syst. Symp., San Juan, Puerto Rico, pp.228-236, Dec. 1994.
• [4] A. Burns, “Scheduling hard real-time systems: a review,” Software Eng. J., vol.6, no.3, pp.116-128, May 1991.
• [5] S.K. Baruah and J.R. Haritsa, “Scheduling for overload in real-time systems,” IEEE Trans. Comput., vol.46, no.9, pp.1034-1039, Sept. 1997.

タイトルに関連する用語 (2件)： SMT ,  スケジューリング