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.
A Specification Translation from Behavioral Specifications to Rewrite Specifications
Masaki NAKAMURA Weiqiang KONG Kazuhiro OGATA Kokichi FUTATSUGI
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2008/05/01
Online ISSN: 1745-1361
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>>
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.