Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support

Min ZHANG  Kazuhiro OGATA  Masaki NAKAMURA  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E94-D   No.5   pp.976-988
Publication Date: 2011/05/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.E94.D.976
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Specification Translation
Keyword: 
specification translation,  CafeOBJ,  Maude,  equational theory specification,  rewrite theory specification,  

Full Text: PDF(919.9KB)>>
Buy this Article




Summary: 
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.