On algebraic specification languages based on modular rewriting systems

• Project/Area Number: 22700027
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Single-year Grants
• Research Field: Software
• Research Institution: Toyama Prefectural University (2011-2012); Kanazawa University (2010)
• Principal Investigator: NAKAMURA Masaki 富山県立大学, 工学部, 講師 (40345658)
• Project Period (FY): 2010 – 2012
• Project Status: Completed (Fiscal Year 2012)
• Budget Amount: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000); Fiscal Year 2012: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2011: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2010: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
• Keywords: 項書換えシステム / 代数仕様 / モジュールシステム / テスト生成 / プログラム変換 / 形式手法 / 仕様変換 / 仕様検証 / UML / 項書き換えシステム / CafeOBJ / Maude

Research Abstract

We studied about term rewriting systems to give an operational semantics of specification execution for algebraic specificationlanguages with sophisticated module systems. Our main result is a termination proving methods based on module structures. Termination is one of the most important properties of term rewriting, which guarantees any specification execution terminates in finite time. By our results, we can prove termination of large and complex algebraic specifications with conditional equations efficiently.

Research Products

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