SMTソルバーを用いた計算機ネットワークにおける周期タスクのリソース割り当てとスケジューリング

摘要

計算機ネットワークにおいて，各計算機のメモリ制約を考慮し，かつすベてのタスクがデッドラインミスを起こさないように各タスクを計算機へ割り当ててスケジュールすることは重要である.本報告では，各計算機のもつメモリ制約とタスクの情報を表す述語論理式を求め，SMT(Satisfiability Modulo Theories)ソルバーを用いてその述語論理式に対する充足可能性判定問題を解いて，タスクの割り当てとスケジュールを行う方法を提案する.%It is important in computer networks to assign each task to a computer in order to have scheduling without deadline miss under constraints of memories. In this paper, we derive logical formulae from information of computers' memory constraints and tasks. By solving a satisfiability problem of the formulae using a Satisfiability Modulo Theories(SMT) solver, we obtain scheduling and resource assignment of tasks.