• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

形式仕様開発支援環境の研究

研究課題

研究課題/領域番号 17700028
研究種目

若手研究(B)

配分区分補助金
研究分野 ソフトウエア
研究機関独立行政法人産業技術総合研究所

研究代表者

清野 貴博  産業技術総合研究所, 情報技術研究部門, 研究員 (10397226)

研究期間 (年度) 2005 – 2007
研究課題ステータス 完了 (2007年度)
配分額 *注記
3,500千円 (直接経費: 3,500千円)
2007年度: 1,000千円 (直接経費: 1,000千円)
2006年度: 1,200千円 (直接経費: 1,200千円)
2005年度: 1,300千円 (直接経費: 1,300千円)
キーワードソフトウェア開発効率化・安定化 / ユーザインターフェース / 形式手法 / ソフトウェア開発効率化・安 / ユーザインターフェイス / 代数仕様 / 項書換え / CafeOBJ / 観測遷移機械
研究概要

本年度は,これまでに提案したツールの発展として,証明譜に基づくテスト生成手法について,提案した(学会発表)。本研究では統合開発環境Eclipseを用いて,ソフトウェアの仕様を記述し,その仕様が望ましい性質を持つことを証明するための支援環境を開発・提案している。しかし,その仕様から実際のソフトウェア開発には距離がある。そこで,仕様記述,証明,ソフトウェア開発をEclipse上で一貫して行うことを目的とし,テスト駆動開発のためのテスト生成手法を提案した。テスト駆動開発とは,ソフトウェアが正しく動作することを確認するためのテスト群を先に開発し,そのテストをパスするようにソフトウェアの開発を進める手法であり,Eclipseはこの手法をサポートするツールとしても有名である。
本研究において提案したテスト生成手法は,既に提案した手法で作成した証明を用いて,テスト群を自動で生成できる。この手法では,生成されたテストにパスしないソフトウェアが開発されると,証明済みの性質を満たさないことが保証される。このため,ソフトウェア開発を形式仕様に基づいて行うことができ,本研究の成果は科学的アプローチに基づく開発手法として,ソフトウェア開発の効率化・安定化につながると期待でぎる。
本年度は,引き続き提案したツールの実装および改良を行った。より,実装を洗練するために多くの改良を行った。これによって証明譜のモデルが整理されたため,同種のソフトウェア開発が容易になると期待される。なお,本補助金による支援終了後も,引き続きツールの改良・保守を行っていく予定である。

報告書

(3件)
  • 2007 実績報告書
  • 2006 実績報告書
  • 2005 実績報告書
  • 研究成果

    (5件)

すべて 2007 2006 2005 その他

すべて 雑誌論文 (3件) 学会発表 (1件) 備考 (1件)

  • [雑誌論文] 形式仕様開発支援環境の研究2006

    • 著者名/発表者名
      清野貴博
    • 雑誌名

      システム検証研究センター 2005年度(平成17年度)研究報告集 PS-2006-006

      ページ: 57-60

    • 関連する報告書
      2006 実績報告書
  • [雑誌論文] A toolkit for generating and displaying proof scores in the OTS/CafeOBJ method.2006

    • 著者名/発表者名
      Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Electronic Notes in Theoretical Computer Science. Vol.147

      ページ: 57-72

    • 関連する報告書
      2005 実績報告書
  • [雑誌論文] Mechanically supporting case analysis for verification of distributed systems.2005

    • 著者名/発表者名
      Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Journal of Pervasive Computing and Communications. Vol.1, No.2

      ページ: 135-145

    • 関連する報告書
      2005 実績報告書
  • [学会発表] OTS/CafeOBJ法における証明譜からのテスト生成2007

    • 著者名/発表者名
      中村 正樹, 清野 貴博
    • 学会等名
      電子情報通信学会ソフトウェアサイエンス研究会
    • 発表場所
      島根大学
    • 年月日
      2007-12-17
    • 関連する報告書
      2007 実績報告書
  • [備考]

    • URL

      http://www.jaist.ac.jp/~t-seino/research/cafeobj/

    • 関連する報告書
      2007 実績報告書

URL: 

公開日: 2005-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi