A Specification Translation from Behavioral Specifications to Rewrite Specifications
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E91-D No.5 pp.1492-1503
- Publication Date
- 2008/05/01
- Publicized
- Online ISSN
- 1745-1361
- DOI
- 10.1093/ietisy/e91-d.5.1492
- Type of Manuscript
- PAPER
- Category
- Fundamentals of Software and Theory of Programs
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Masaki NAKAMURA, Weiqiang KONG, Kazuhiro OGATA, Kokichi FUTATSUGI, "A Specification Translation from Behavioral Specifications to Rewrite Specifications" in IEICE TRANSACTIONS on Information,
vol. E91-D, no. 5, pp. 1492-1503, May 2008, doi: 10.1093/ietisy/e91-d.5.1492.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1093/ietisy/e91-d.5.1492/_p
Copy
@ARTICLE{e91-d_5_1492,
author={Masaki NAKAMURA, Weiqiang KONG, Kazuhiro OGATA, Kokichi FUTATSUGI, },
journal={IEICE TRANSACTIONS on Information},
title={A Specification Translation from Behavioral Specifications to Rewrite Specifications},
year={2008},
volume={E91-D},
number={5},
pages={1492-1503},
abstract={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.},
keywords={},
doi={10.1093/ietisy/e91-d.5.1492},
ISSN={1745-1361},
month={May},}
Copy
TY - JOUR
TI - A Specification Translation from Behavioral Specifications to Rewrite Specifications
T2 - IEICE TRANSACTIONS on Information
SP - 1492
EP - 1503
AU - Masaki NAKAMURA
AU - Weiqiang KONG
AU - Kazuhiro OGATA
AU - Kokichi FUTATSUGI
PY - 2008
DO - 10.1093/ietisy/e91-d.5.1492
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E91-D
IS - 5
JA - IEICE TRANSACTIONS on Information
Y1 - May 2008
AB - 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.
ER -
English
