モジュラー書換え理論に基づく代数型ソフトウェア開発言語の構築

• 研究課題/領域番号: 22700027
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 富山県立大学 (2011-2012); 金沢大学 (2010)
• 研究代表者: 中村 正樹 富山県立大学, 工学部, 講師 (40345658)
• 研究期間 (年度): 2010 – 2012
• 研究課題ステータス: 完了 (2012年度)
• 配分額: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円); 2012年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2011年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2010年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
• キーワード: 項書換えシステム / 代数仕様 / モジュールシステム / テスト生成 / プログラム変換 / 形式手法 / 仕様変換 / 仕様検証 / UML / 項書き換えシステム / CafeOBJ / Maude

研究概要

モジュールシステムを備えた代数仕様言語に適した項書換えシステムによる仕様実行に関する基礎的研究を行い,モジュール構造に基づく効率的な停止性判定手法を提案した.停止性は,項書換えシステムの最も重要な性質の1つで,任意の実行の有限時間内の停止性を保証する.本手法を用いることで,大規模複雑な代数仕様に対して,効率的に停止性を示すことが可能となり,モジュラーな代数型言語の開発の重要な基礎を与えた.

研究成果

• [雑誌論文] On ProvingOperational TerminationIncrementally with ModularConditional Dependency Pairs (2013)
  • 著者名/発表者名: Masaki Nakamura, KazuhiroOgata, andKokichi Futatsugi
  • 雑誌名: IAENGInternational Journal of ComputerScience 巻: 40 ページ: 117-123
  • URL: http://www.iaeng.org/IJCS/issues_v40/issue_2/index.html
  • 査読あり
• [雑誌論文] Translation of StateMachines from Equational Theoriesinto Rewrite Theories with ToolSupport (2011)
  • 著者名/発表者名: Min Zhang, Kazuhiro Ogata, MasakiNakamura
  • 雑誌名: IEICE Transactions94-D(5) ページ: 976-988
  • URL: http://dx.doi.org/10.1587/transinf.E94.D.976
• [雑誌論文] Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support (2011)
  • 著者名/発表者名: Min Zhang, Kazuhiro Ogata, Masaki Nakamura
  • 雑誌名: IEICE Transactions on Information and Systems 巻: E94-D 号: 5 ページ: 976-988
  • DOI: 10.1587/transinf.E94.D.976
  • NAID: 10029506958
  • ISSN: 0916-8532, 1745-1361
  • 査読あり
• [雑誌論文] Reducibility ofoperation symbols in term rewritingsystems and its application tobehavioral specifications (2010)
  • 著者名/発表者名: Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
  • 雑誌名: Journal of Symbolic Computation 巻: 45 ページ: 551-573
  • URL: http://dx.doi.org/10.1016/j.jsc.2010.01.008
• [雑誌論文] Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications. (2010)
  • 著者名/発表者名: Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
  • 雑誌名: Journal of Symbolic Computation 巻: 45 ページ: 551-573
  • NAID: 120003338960
  • 査読あり
• [学会発表] IncrementalProofs of Operational Terminationwith ModularConditional DependencyPairs (2013)
  • 著者名/発表者名: Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
  • 学会等名: Proceedings of theInternational MultiConference ofEngineers and Computer Scientists2013
  • 発表場所: Hong Kong, China
• [学会発表] A HierarchicalApproach toOperational Terminationof Algebraic Specifications, Proceedings of the InternationalConference on Electronics (2013)
  • 著者名/発表者名: Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
  • 学会等名: Information andCommunication, ICEIC 2013
  • 発表場所: Bali, Indonesia
• [学会発表] On DescribingTerminating AlgebraicSpecificationsBased on Their Models (2013)
  • 著者名/発表者名: Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
  • 学会等名: Proceedings oftheInternational MultiConference ofEngineers and Computer Scientists2012, IMECS 2012
  • 発表場所: Hong Kong, China
• [学会発表] Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs (2013)
  • 著者名/発表者名: NAKAMURA Masaki
  • 学会等名: The International MultiConference of Engineers and Computer Scientists 2013
  • 発表場所: Hong Kong, China
• [学会発表] A Hierarchical Approach to Operational Termination of Algebraic Specifications (2013)
  • 著者名/発表者名: NAKAMURA Masaki
  • 学会等名: The 12th International Conference on Electronics, Information, and Communication (ICEIC 2013)
  • 発表場所: Bali, Indonesia
• [学会発表] On Describing Terminating Algebraic Specifications Based on Their Models (2012)
  • 著者名/発表者名: Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
  • 学会等名: International MultiConference of Engineers and Computer Scientists 2012
  • 発表場所: China, Hong Kong
  • 年月日: 2012-03-16
• [学会発表] Specification Translation of State Machines from Equational Theories in to Rewrite Theories (2010)
  • 著者名/発表者名: Min Zhang
  • 学会等名: 12th International Conference on Formal Engineering Methods, ICFEM 2010
  • 発表場所: Shanghai, China
  • 年月日: 2010-11-19
• [学会発表] OTS/CafeOBJ 法に基づく並行システムの実装とテスト生成 (2010)
  • 著者名/発表者名: 清野貴博, 中村正樹
  • 学会等名: 電子情報通信学会技術研究報告
  • 発表場所: 信学技報
• [学会発表] OTS/CafeOBJ 法における証明譜からのテスト生成 (2010)
  • 著者名/発表者名: 中村正樹
  • 学会等名: 第20回形式手法研究会
  • 発表場所: 専修大学神田校舎
• [学会発表] Specification Translationof State Machines from EquationalTheories into Rewrite Theories (2010)
  • 著者名/発表者名: Min Zhang, KazuhiroOgata and MasakiNakamura
  • 学会等名: 12thInternational Conference on FormalEngineering Methods (ICFEM2010)Lecture Notes in Computer Science
  • 発表場所: Shanghai, China.