Abstract
This paper presents a strategy together with tool support for the translation of state machines from equational theories into rewrite theories, aiming at automatically generating rewrite theory specifications. Duplicate effort can be saved on specifying state machines both in equational theories and rewrite theories, when we incorporate the theorem proving facilities of CafeOBJ with the model checking facilities of Maude. Experimental results show that efficiencies of the generated specifications by the proposed strategy are significantly improved, compared with those that are generated by three other existing translation strategies.
| Original language | English |
|---|---|
| Pages (from-to) | 976-988 |
| Number of pages | 13 |
| Journal | IEICE Transactions on Information and Systems |
| Volume | E94-D |
| Issue number | 5 |
| DOIs | |
| State | Published - May 2011 |
| Externally published | Yes |
Keywords
- CafeOBJ
- Equational theory specification
- Maude
- Rewrite theory specification
- Specification translation