A specification translation from behavioral specifications to rewrite specifications

被引：10

作者：

Nakamura, Masaki ^{[1
]}

Kong, Weiqiang ^{[1
]}

Gata, Kazuhiro ^{[1
]}

Futatsugi, Kokichi ^{[1
]}

机构：

[1] Japan Adv Inst Sci & Technol, Sch Informat Sci, Nomi 9231211, Japan

来源：

IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS | 2008年 / E91D卷 / 05期

关键词：

specification translation; verification; algebraic specification; behavioral specification; rewirte specification; CafeOBJ; Maude;

D O I：

10.1093/ietisy/e91-d.5.1492

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：1492 / 1503

页数：12

共 17 条

[1]

Aguirre N, 2007, LECT NOTES COMPUT SC, V4591, P1

[2]

Chandy K.M., 1988, Parallel Program Design: A Foundation

[3]

Diaconescu R, 1998, AMAST SERIES COMPUTI, V6

[4]

FUTATSUGI K, 1985, P 12 ACM S PRINC PRO, P52

[5]

GOGUEN JA, 2000, SOFTWARE ENG OBJ ALG

[6]

HAXTHAUSEN AE, 2006, P 1 AS WORK C VER SO, P209

[7]

KONG W, 2006, THESIS JAPAN ADV I S

[8]

NAKAMURA M, 2006, SS200613 IEICE

[9]

Ogata K, 2005, PDCAT 2005: Sixth International Conference on Parallel and Distributed Computing, Applications and Technologies, Proceedings, P416

[10]

Ogata K, 2004, LECT NOTES COMPUT SC, V3233, P45

← 1 2 →