Formal Verification of Graph Grammars using Mathematical Induction

被引：6

作者：

da Costa, Simone Andre ^{[1
]}

Ribeiro, Leila ^{[1
]}

机构：

[1] Univ Fed Rio Grande do Sul, Inst Informat, Porto Alegre, Brazil

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2009年 / 240卷

关键词：

Graph grammars; mathematical induction; formal verification;

D O I：

10.1016/j.entcs.2009.05.044

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Graph grammars are a formal description technique suitable for the specification of distributed and reactive systems. Model-checking of graph grammars is currently supported by various approaches. However, in many situations the use of this technique can be very time and space consuming, hindering the verification of properties of many systems. This work proposes a relational and logical approach to graph grammars that allows formal verification of systems using mathematical induction. We use relational structures to define graph grammars and first-order logic to model graph transformations. This approach allows proving properties of systems with infinite state-spaces.

引用

页码：43 / 60

页数：18

共 21 条

[1]

Baldan P, 2002, LECT NOTES COMPUT SC, V2505, P14

[2] Unfolding semantics of graph transformation [J].

Baldan, Paolo ;

Corradini, Andrea ;

Montanari, Ugo ;

Ribeiro, Leila .

INFORMATION AND COMPUTATION, 2007, 205 (05) :733-782

[3]

Baresi L, 2006, LECT NOTES COMPUT SC, V4178, P306

[4]

Behrmann G, 2004, LECT NOTES COMPUT SC, V3185, P200

[5]

Clarke E, 2001, LECT NOTES COMPUT SC, V2000, P176

[6] Formal methods: State of the art and future directions [J].

Clarke, EM ;

Wing, JM .

ACM COMPUTING SURVEYS, 1996, 28 (04) :626-643

[7]

Courcelle B, 2004, LECT NOTES COMPUT SC, V3340, P1

[8] MONADIC 2ND-ORDER DEFINABLE GRAPH TRANSDUCTIONS - A SURVEY [J].

COURCELLE, B .

THEORETICAL COMPUTER SCIENCE, 1994, 126 (01) :53-75

[9]

Dotti FL, 2003, LECT NOTES COMPUT SC, V2884, P261

[10]

Dotti FL, 2000, INT FED INFO PROC, V49, P45

← 1 2 3 →