For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support
Min ZHANG Kazuhiro OGATA Masaki NAKAMURA
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2011/05/01
Online ISSN: 1745-1361
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Specification Translation
specification translation, CafeOBJ, Maude, equational theory specification, rewrite theory specification,
Full Text: PDF(919.9KB)>>
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.