A Specification Translation from Behavioral Specifications to Rewrite Specifications

Masaki NAKAMURA  Weiqiang KONG  Kazuhiro OGATA  Kokichi FUTATSUGI  

IEICE TRANSACTIONS on Information and Systems   Vol.E91-D   No.5   pp.1492-1503
Publication Date: 2008/05/01
Online ISSN: 1745-1361
DOI: 10.1093/ietisy/e91-d.5.1492
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Fundamentals of Software and Theory of Programs
specification translation,  verification,  algebraic specification,  behavioral specification,  rewirte specification,  CafeOBJ,  Maude,  

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

There are two ways to describe a state machine as an algebraic specification: a behavioral specification and a rewrite specification. In this study, we propose a translation system from behavioral specifications to rewrite specifications to obtain a verification system which has the strong points of verification techniques for both specifications. Since our translation system is complete with respect to invariant properties, it helps us to obtain a counter-example for an invariant property through automatic exhaustive searching for a rewrite specification.