On a formal verification system based on modular term rewriting

基于模块化术语重写的形式化验证系统

• 批准号: 18700024
• 负责人: NAKAMURA Masaki
• 金额: $ 2.39万
• 依托单位: Kanazawa University (2008)Japan Advanced Institute of Science and Technology (2006-2007)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2006
• 资助国家: 日本
• 起止时间: 2006 至 2008
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18700024/
• 关键词: 形式手法; 検証システム; 項書換えシステム; 代数仕様; モジュールシステム; 仕様変換; ソフトウェアテスト; 自動ソフトウェアテスト; 項書換システム; 項書き換えシステム

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

This study is aimed at the development of a new system of computer science. This is the first time that we've seen this. The research results of the research on the development of language and language are obtained from the research on the development of language and language, the integration of different demonstration technologies, the basic theory of demonstration technology, and the whole development project.

项目成果

On equality predicates in algebraic specification languages

• DOI: 10.1007/978-3-540-75292-9_26
• 发表时间: 2007-09
• 作者: Nakamura Masaki;Futatsugi Kokichi

Generating test cases for invariant properties from proof scores in the OTS/CafeOBJ method

根据 OTS/CafeOBJ 方法中的证明分数生成不变属性的测试用例

• 发表时间: 2009
• 期刊: IEICE Transactions on Information and Systems vol.5
• 作者: Masaki Nakamura;Takahiro Seino
• 通讯作者: Takahiro Seino

User-Defined On-Demand Matching

用户自定义按需匹配

• 发表时间: 2009
• 期刊: IEICE Transactions 92-D(7)
• 作者: Masaki Nakamura;Kazuhiro Ogata;Kokichi Futatsugi
• 通讯作者: Kokichi Futatsugi

モジュラーな代数仕様言語のための項書き換えシステム

模块化代数规范语言的术语重写系统

• 发表时间: 2006
• 期刊: コンピュータソフトウェア(日本ソフトウェア科学会論文誌) 23・3
• 作者: 中村正樹;二木厚吉
• 通讯作者: 二木厚吉

実行可能な代数仕様の停止性証明について

关于可执行代数规范的停止证明

• 发表时间: 2007
• 作者: 中村 正樹;二木 厚吉
• 通讯作者: 二木 厚吉