モジュラーな項書き換えシステムに基づく仕様検証システムの開発

2008 年度 研究成果報告書

• 研究課題/領域番号: 18700024
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 金沢大学 (2008); 北陸先端科学技術大学院大学 (2006-2007)
• 研究代表者: 中村 正樹 金沢大学, 電子情報学系, 助教 (40345658)
• 研究期間 (年度): 2006 – 2008
• キーワード: 形式手法 / 検証システム / 項書換えシステム / 代数仕様 / モジュールシステム / 仕様変換 / ソフトウェアテスト

研究概要

本研究では, モジュラーな項書換えシステムに基づく仕様検証システムの開発を行った. これにより, 特に仕様作成, 実行, 検証時におけるデータ仕様の扱いが容易となり, 形式仕様言語の幅広い利用を促す研究成果が得られた. また, 仕様から実装を得るためのツールの開発, 異なる検証技術の融合技術, 検証エンジンの基礎理論など, ソフトウェア開発工程全体を取り扱うことが可能な形式仕様言語の構築へとつながる研究成果が得られた.

研究成果

• [雑誌論文] Generating test cases for invariant properties from proof scores in the OTS/CafeOBJ method (2009)
  • 著者名/発表者名: Masaki Nakamura, Takahiro Seino
  • 雑誌名: IEICE TRANSACTI ONS on Information and Systems Vol.E92-D, No.5(in press)
  • 査読あり
• [雑誌論文] User-defined on-demand matching (2009)
  • 著者名/発表者名: Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
  • 雑誌名: IEICE TRANSACTIONS on Information and Systems Vol.E92-D, No.7(in press)
  • 査読あり
• [雑誌論文] A specification translation from behavioral specifications to rewrite specifications (2008)
  • 著者名/発表者名: Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
  • 雑誌名: IEICE TRANSACTIONS on Information and Systems Vol.E91-D, No.5 ページ: 492-1503
  • 査読あり
• [雑誌論文] Creme: An Automatic Invariant Prover Of Behavioral Specifications (2007)
  • 著者名/発表者名: Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, and Kokichi Futatsugi
  • 雑誌名: International Journal of Software Engineering and Knowledge Engineering(IJSEKE) Vol.17, No. 6 ページ: 783-804
  • 査読あり
• [雑誌論文] 実行可能な代数仕様の停止性証明について (2007)
  • 著者名/発表者名: 中村正樹, 二木厚吉
  • 雑誌名: 情報科学技術レターズ Vol.6 ページ: 27-30
  • 査読あり
• [雑誌論文] Elimination Transformations for Associative-Commutative Rewriting Systems (2006)
  • 著者名/発表者名: K. Kusakari, M. Nakamura and Y. Toyama
  • 雑誌名: Journal of Automated Reasoning Vol. 37, No. 3 ページ: 205-229
  • 査読あり
• [雑誌論文] A Behavioral Specificationof Imperative Programming Languages (2006)
  • 著者名/発表者名: M. Nakamura, M. Watanabe and K. Futatsugi
  • 雑誌名: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences Vol. E89-A, No.6 ページ: 1558-1565
  • 査読あり
• [雑誌論文] モジュラーな代数仕様言語のための項書き換えシステム (2006)
  • 著者名/発表者名: 中村正樹, 二木厚吉
  • 雑誌名: コンピュータソフトウェア Vol. 23, No. 3 ページ: 35-50
  • 査読あり
• [学会発表] OTS/CafeOBJ法における証明譜からのテスト生成 (2007)
  • 著者名/発表者名: 中村正樹,清野貴博
  • 学会等名: ソフトウェアサイエンス研究会(SS)
  • 発表場所: 松江
  • 年月日: 2007-12-17
• [学会発表] On equality predicates in algebraic specification languages (2007)
  • 著者名/発表者名: Masaki Nakamura and Kokichi Futatsugi
  • 学会等名: the 4th International Colloquium on Theoretical Aspects of Computing
  • 発表場所: Macau
  • 年月日: 2007-09-26
• [学会発表] 実行可能な代数仕様の停止性証明について (2007)
  • 著者名/発表者名: 中村正樹,二木厚吉
  • 学会等名: 第6回情報科学技術フォーラム(FIT)
  • 発表場所: 豊田
  • 年月日: 2007-09-07
• [学会発表] A complete specification transformation from OTS/CafeOBJ to OTS/Maude (2006)
  • 著者名/発表者名: Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
  • 学会等名: ソフトウェアサイエンス研究会(SS)
  • 発表場所: 岡山
  • 年月日: 2006-06-22