On algebraic specification languages based on modular rewriting systems

基于模块化重写系统的代数规约语言

• 批准号: 22700027
• 负责人: NAKAMURA Masaki
• 金额: $ 2.41万
• 依托单位: Toyama Prefectural University (2011-2012)Kanazawa University (2010)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2010
• 资助国家: 日本
• 起止时间: 2010 至 2012
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22700027/
• 关键词: 項書換えシステム; 代数仕様; モジュールシステム; テスト生成; プログラム変換; 形式手法; 仕様変換; 仕様検証; UML; 項書き換えシステム; CafeOBJ; Maude

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.

本文研究了项重写系统，给出了具有复杂模块系统的代数规格说明语言的规格说明执行的操作语义。我们的主要结果是基于模块结构的终止性证明方法。可终止性是项重写的重要特性之一，它保证了任何规范的执行都能在有限时间内终止。利用我们的结果，我们可以有效地证明大型复杂代数规格的条件方程的终止性。

项目成果

Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications.

术语重写系统中操作符号的可约化性及其在行为规范中的应用。

• 发表时间: 2010
• 期刊: Journal of Symbolic Computation
• 影响因子: 0.7
• 作者: Masaki Nakamura;Kazuhiro Ogata;Kokichi Futatsugi
• 通讯作者: Kokichi Futatsugi

OTS/CafeOBJ 法における証明譜からのテスト生成

OTS/CafeOBJ 方法中的证明分数生成测试

• 发表时间: 2010
• 作者: 中川博之;大須賀昭彦;本位田真一;中村正樹
• 通讯作者: 中村正樹

Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support

在工具支持下将状态机从方程理论转化为重写理论

• DOI: 10.1587/transinf.e94.d.976
• 发表时间: 2011
• 期刊: IEICE Transactions on Information and Systems
• 影响因子: 0.7
• 作者: Min Zhang;Kazuhiro Ogata;Masaki Nakamura
• 通讯作者: Masaki Nakamura

OTS/CafeOBJ 法に基づく並行システムの実装とテスト生成

基于OTS/CafeOBJ方法的并发系统实现和测试生成

• 发表时间: 2010
• 作者: 清野貴博;中村正樹
• 通讯作者: 中村正樹

On DescribingTerminating AlgebraicSpecificationsBased on Their Models

关于基于模型描述终止代数规范

• 发表时间: 2013
• 作者: Masaki Nakamura;Kazuhiro Ogata;Kokichi Futatsugi
• 通讯作者: Kokichi Futatsugi