On a formal verification system based on modular term rewriting

• Project/Area Number: 18700024
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Single-year Grants
• Research Field: Software
• Research Institution: Kanazawa University (2008); Japan Advanced Institute of Science and Technology (2006-2007)
• Principal Investigator: NAKAMURA Masaki Kanazawa University, 電子情報学系, 助教 (40345658)
• Project Period (FY): 2006 – 2008
• Project Status: Completed (Fiscal Year 2008)
• Budget Amount: ¥3,730,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥330,000); Fiscal Year 2008: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2007: ¥1,100,000 (Direct Cost: ¥1,100,000); Fiscal Year 2006: ¥1,200,000 (Direct Cost: ¥1,200,000)
• Keywords: 形式手法 / 検証システム / 項書換えシステム / 代数仕様 / モジュールシステム / 仕様変換 / ソフトウェアテスト / 自動ソフトウェアテスト / 項書換システム / 項書き換えシステム

Research Abstract

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

Research Products

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