IPA


開発成果一覧へ





2004年度第2回未踏ソフトウェア創造事業  採択案件評価書


 



1.担当PM

 

 坂村 健  (東京大学大学院 情報学環 教授)



2.採択者氏名


 代表者

 永藤 直行 (有限会社プレシステム 代表取締役)

共同開発者

 なし



3.プロジェクト管理組織


 株式会社インスパイア



4.委託金支払額

 
 8,711,417円



5.テーマ名

 

 組込みソフトウェアのためのテスティングツールの開発



6.関連Webサイト


 http://www4.ocn.ne.jp/~presys



7.テーマ概要


 組み込みシステムソフトウェアの検証・試験フェーズ(ここで,「検証」とはモデルを対象とした検査を,「試験」とはプログラムを対象とした検査をいう。「モデル」とはシステムの振る舞いを示す状態遷移マシンをいい,「プログラム」とはモデルに基づいて実装された実動するシステムをいう)では,次のことが課題として取り上げられる。
  1. 試験時間に関する課題
  2. 検証・試験の質に関する課題
 第1項の試験時間に関する課題とは,限られた開発期間の中で検証や試験に充当できる時間が限られているため,満足のいくレベルまで検証や試験ができないという課題である。第2項の検証・試験の質に関する課題とは,検証や試験の質が検証・試験者の経験に依存した方式に陥りがちであり,検証や試験にばらつきが生じてしまうという課題である。第2項の解決手法として,モデルの検証ツールとしてSPINやFDRなどがすでに知られている。しかしこれらはモデルの検査を行うためのツール(以下これを「モデル検証器」という)である。本プロジェクトでは,モデル検証器の検証対象をプログラムの試験にまで拡張したテスティングツールの開発を行う。これにより,第2項にあげた試験の質の向上とあわせて第1項にあげた試験時間の短縮に寄与することをめざす。
 組み込みソフトウェアの開発方式としては,現在でも直接ポーティングする方法が主流である。組み込みソフトウェア開発を上流工程から行うという試みは,新しい手法となりえる。また既存のソフトウェア資源の流用につながるという期待もある。



8.採択理由

 

 組み込みソフトウェアの開発方式としては,現在でも直接ポーティングする方法が主流である。組み込みソフトウェア開発を上流工程から行うという試みは,新しい手法となりえる。また既存のソフトウェア資源の流用につながる可能性もあるため。同様の応募が他にもあったが,この応募の開発計画が相対的に着実であり,手堅く感じられたため採用とした。




9.開発目標


  本プロジェクトの開発目標は,プログラムのソースコードを対象としてモデルの検証を行うモデル検証器を開発することにある。そのために必要な要素は以下の通りである。
  ・モデル検証器インタプリタ
  ・モデル記述言語
  ・GDBインタフェース
  ・LTL記述言語
  ・LTL2CCS変換器



10.進捗概要


 プロジェクトを開始するに当たって,プロジェクトマネージャはまず組み込みシステムに特有の問題を明確にするために,組み込みシステムを1つ作ってみて,そのうえで組み込みシステムの検証に必要な事項をあげてみるよう指摘した。
 組み込み開発環境であるT-Engineを開発ターゲットとして,T-Engine開発環境に付属するデバッガ gdb を用いて,9.の開発目標に掲げた各要素は,一通り実装を完了し,サンプルプログラムの無限ループを検出するなど,モデル検証器が動作するレベルに達した。モデル記述言語設計に時間がかかったため,サンプルの準備などがまだ充分とはいえない。また,プロジェクトマネージャが当初から提起していた,組み込みシステムに特有の問題に対する検証方法を提示する段階までは至らなかった。



11.成果


 上記の9.開発目標に掲げた以下の要素を有するモデル検証器を開発した。
  ・モデル検証器インタプリタ
  ・モデル記述言語
  ・GDBインタフェース
  ・LTL記述言語
  ・LTL2CCS変換器
 成果物は開発者のサイト http://www4.ocn.ne.jp/~presysに公開されている。




12.プロジェクト評価


 組み込みソフトウェアの開発方式としては,現在でも直接ポーティングする方法が主流である。組み込みソフトウェア開発を上流工程から行うという本プロジェクトの試みは,新しい手法となりえる。また既存のソフトウェア資源の流用につながるという期待もある。今回の成果物は,組み込みソフトウェア開発を上流工程から行う試みの,必要最低限の部分を実現したものと言える。それが動作するレベルまで達したことは評価に値する。
 しかし,今回の成果物は組み込みシステムで問題になる複数のタスク間の通信や排他制御,またリアルタイムに発生する割り込みに対する制御などの問題を扱えることを示せてはいない。また組み込みシステムの開発者は今回の成果物が要求しているプロセス代数などの知識を持ち合わせているとは言い難い。さらに検証するモデル記述に間違いがあれば検証そのものが破綻してしまうため,モデル記述を正確に行うための支援ツールが不可欠である。
 当初からプロジェクトマネージャが提起していた,先に述べたような組み込みシステムならでは問題に対する検証方法が提示されなかったことは残念である。これは今後の課題となろう。



13.今後の課題


 今後,複数のタスク間の通信や排他制御,またリアルタイムに発生する割り込みに対する制御など,組み込み特有の問題にモデル検証がいかに対処するのか検討を進める必要がある。また,一般の組み込みシステム開発者が利用できるようにするには,モデル記述を正確に行うための支援ツールやマニュアルなどの整備が不可欠である。


  ページトップへ