@inproceedings{eaed73a0f7ad47338f46463392b5d508,
title = "Specification translation of state machines from equational theories into rewrite theories",
abstract = "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.",
keywords = "Algebraic specification, CafeOBJ, Maude, automatic translation, equational theory, rewrite theory",
author = "Min Zhang and Kazuhiro Ogata and Masaki Nakamura",
year = "2010",
doi = "10.1007/978-3-642-16901-4\_44",
language = "英语",
isbn = "3642169007",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "678--693",
booktitle = "Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Proceedings",
note = "12th International Conference on Formal Engineering Methods, ICFEM 2010 ; Conference date: 17-11-2010 Through 19-11-2010",
}