| Research Abstract |
今年度は, 1. シングルCPU上で動作するリアルタイムオペレーティングシステム(RTOS)の検証実験, 及び, 2. マルチコアCPU上で動作するソフトウェアの検証実験を行った. 1のRTOSの検証実験では, 車載システム用のOSであるOSEK/VDXを対象とした. OSは様々な使われ方をするため, その使われ方のバリエーションをUMLにより整理して記述する. そして, その記述からモデル検査のための記述を複数自動生成するアルゴリズムを提案した. このアルゴリズムでは, 個々の使われ方毎に1つのモデル検査用記述を生成する. そのため, 検査するバリエーションが多くなると, 大量のモデル検査用記述が生成される. そこで, 現在, それらの記述を計算機クラスタなどを用いて検証する方法について検討を行っている. 2の検証実験では, Playstation 3に搭載されているCellプロセッサ上で動作するプログラムを対象とし, パフォーマンス要件をモデル検査ツールを用いて検証する実験を行った. Cellプロセッサでは, SPE, および, PPEと呼ばれる, 異る機能を持つコアが複数搭載され, それらが高速なバスで接続されている. このようなプロセッサ向けソフトウェアでは, 適切に処理を振り分け, バスの遅延を考慮し, 効果的に並行実行する必要がある. そこで, Cellプロセッサ上で並行実行させる仕組みを設計モデルとして記述し, モデル検査ツールを用いて, パフォーマンスの優劣を事前に評価する実験を行った. これらの実験により, 検証対象の外側, いわゆる, 環境のモデルが重要であることと, 複数のコアを使う場合, 機能要件よりは, パフォーマンス要件の方が重要であることがわかった, 今後, この2点に焦点を当て, 形式化を行う予定である.
|
