A Specification Translation from Behavioral Specifications to Rewrite Specifications
Masaki Nakamura, Weiqiang Kong, K. OGATA, Kokichi Futatsugi · IEICE Transactions on Information and Systems · 2008
There are two ways to describe a state machine as an algebraic specification: a behavioral specification and a rewrite specificaon.In this study, we propose a translation system from behavioral specifations 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 automatc exhaustive searching for a rewrite specification.