\section{ まとめ}

May Core Architecture のプログラムを作成する手法として、
シーケンシャルなCの記述を、CbCに分解する手法を提案し実践してみた。
また、その手法に対するテスト及び検証法について述べた。

CbCでは、モデル検査部と実装部分を混在し、同時にプログラムすることが
出来るので、並列実行部分を作成しながら、それをテストするための
モデル検査部を作成していくことが可能である。

現在のモデル検査部で、SPIN と Java Path Finder の中間的な性能を
得ることが出来ているが、より高性能なアルゴリズムを実装する必要が
ある。

Cerium Rendering Engine はCell上で動作しているが、テスト及び
モデル検査は行っていないので、これらを実装して、実際の効果を
調べることが必要である。