|
JAIST Repository >
b. 情報科学研究科・情報科学系 >
b10. 学術雑誌論文等 >
b10-1. 雑誌掲載論文 >
このアイテムの引用には次の識別子を使用してください:
http://hdl.handle.net/10119/9946
|
| タイトル: | Specification Translation of State Machines from Equational Theories into Rewrite Theories |
| 著者: | Zhang, Min
Ogata, Kazuhiro
Nakamura, Masaki |
| キーワード: | Algebraic specification
automatic translation
rewrite theory
equational theory
CafeOBJ
Maude |
| 発行日: | 2010-11-09 |
| 出版者: | Springer |
| 誌名: | Lecture Notes in Computer Science |
| 巻: | 6447/2010 |
| 開始ページ: | 678 |
| 終了ページ: | 693 |
| DOI: | 10.1007/978-3-642-16901-4_44 |
| 抄録: | Specifications of state machines in CafeOBJ are called equational theory specifications (EQT Specs) which are based on equational logic, and in Maude are called rewrite theory specifications (RWT Specs) which are based on rewriting logic. The translation from EQT Specs to RWT Specs achieves the collaboration between CafeOBJ’s theorem proving facilities and Maude’s model checking facilities. However, translated specifications by existing strategies are of inefficiency and rarely used for model checking in practice. This paper defines a specific class of EQT Specs called EADS Specs, and proposes a strategy for the translation from EADS Specs to RWT Specs. It is proved that translated specifications by the strategy are more efficient than those by existing strategies. |
| Rights: | This is the author-created version of Springer, Min Zhang, Kazuhiro Ogata and Masaki Nakamura, Lecture Notes in Computer Science, 6447/2010, 2010, 678-693. The original publication is available at www.springerlink.com, http://dx.doi.org/10.1007/978-3-642-16901-4_44 |
| URI: | http://hdl.handle.net/10119/9946 |
| 資料タイプ: | author |
| 出現コレクション: | b10-1. 雑誌掲載論文 (Journal Articles)
|
このアイテムのファイル:
| ファイル |
記述 |
サイズ | 形式 |
|---|
| 15831.pdf | | 439Kb | Adobe PDF | 見る/開く |
|
当システムに保管されているアイテムはすべて著作権により保護されています。
|
