6.2 今後の課題
• 時間オートマトンの枠組みを自動化 ??節で説明したコードの自動生成を前処理機 械（又はコンパイラ）によって本当に自動的に生成できるように実装を追加する．
• Cellチップ全体のパフォーマンスの検証実験 本研究はまだ1つのコアしか考察し ていないが，本当に実用の実験は各コア間の通信も含めたモデルに対してのパフォー マンスの検証である．そして，できるだけそれらのパフォーマンス性質を実際のCell チップとプログラムで確認した方が良いと考えられる．
• 状態爆発問題を減少 Partial order reduction のような仕組みで、長いピリオドに 対して最初と最後のティックのみを調べ、その中間のティックを抽象化する．
参考文献
[1] Sony Computer Entertainment Incorporated. Cell Broadband Engineアーキテクチャ Version 1.01, 2006年10月3日.
[2] 齊藤智隆. Cell と共に歩む. 東芝レビュー 61巻6号，特集：Cellからの始まり, 2006 年6月.
付 録 A 用語
マルチコア・プロセッサ(英：Multi-core Processor) 複数のコア
ヘテロジニアス・マルチコア・プロセッサ (英：Heterogeneous Multi-core Proces-sor)(略：HMCP) 複数個のコア
モデル検査(英：Model Checking) 複数のコア
多重バッファリング(英：Multiple Buffering/Multi-buffering) 複数の並列処理ユニ ットの平行性を向上するために複数のバッファを用いてデータを保管する．
2重バッファリング(英：Double Buffering) 多重ぶっふぁリングの特別な場合で，２つ のバッファを用いる．
付 録 B API
本章ではCell用プログラムの応用モデル，いわゆる「ユーザ」，へのモデル・インタフェー ス1を記述する．「MFCパッケージ」はSPEの基盤モデル，つまりMFCとそのSPUへの 結びの仕組みを提供する．この基盤モデルは待機オートマトンの枠組みと時間オートマ トンの枠組みとどちらでも組み合わせて利用できる．「Waitパッケージ」は待機オートマ トンの枠組みを提供する．「Clockパッケージ」は時間オートマトンの枠組みを提供する．
APIの記述し方について，ユーザが利用できる要素は「•」目印が付いた箇条文で記述し，
ユーザによって定義・指定する必要な要素は「◦」目印が付いた箇条文で記述する．
B.1 MFC パッケージ
◦ SPU()：SPUのプロセスの処理内容である．
◦ MFCPutDelay()：putコマンドの実行時に，ユーザが監視する作業の内容である．こ のサブルーチンはputコマンドが実行されるとき毎に呼び出される．
• pMFC_current_cmd：MFCは処理しているコマンド，又はMFCは最後に処理した コマンドである．
• MFCコマンドの実行順序の非決定性により，MFCコマンド・キューは必ずFIFO キューではないので，Promelaのメッセージ・バッファが使えなく，１つのコマ ンドの配列SPUCmdQ[]と１つのキュー管理のプロセスMFCCmdReceiver()によって モデル化する．
• SPUがMFCコマンドを発行する仕組みをコマンドのランデブー・チャンネルMFCCmd_ch を通してMFCCmdReceiver()へコマンドのメッセージを送ることでモデル化する．
• MFCのみの振舞いを検査するために，ランダムのコマンドを発行するSPUプロセ スを用意する．このプロセスはPromelaの非決定選択によってモデル化する．
1Application Model Interfaceの略は「AMI」はずである．しかし，分かり易さのために本論文は「AMI」
の代わりに，普及された用語Application Program Interfaceの略「API」を用いて記述する．