Towards Automated Software Verification and Validation

被引：2

作者：

Asadollahi, Somayeh ^{[1
]}

Rafe, Vahid ^{[1
]}

Rafeh, Reza ^{[1
]}

机构：

[1] Islamic Azad Univ, Dept Comp Engn, Branch Malayer, Tehran, Iran

来源：

PROCEEDINGS OF THE 2009 INTERNATIONAL CONFERENCE ON COMPUTER TECHNOLOGY AND DEVELOPMENT, VOL 1 | 2009年

关键词：

Model Checking; Layered Graph Transformation Systems; LTL; Bogor; AGG; GRAPH TRANSFORMATION;

D O I：

10.1109/ICCTD.2009.164

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Today, it's an important requirement to have software systems without any bug. Model checking has proven to be a viable solution for reasoning about behavior properties of many different software artifacts. In this paper, we present an efficient solution to verify software models which formally specified by layered graph transformation systems - special types of graph transformation systems - using a model checker called Bogor.

引用

页码：206 / 210

页数：5

共 15 条

[1]

Andrade L, 2003, LECT NOTES COMPUT SC, V2755, P1

[2]

[Anonymous], AGG

[3]

Baldan P, 2005, LECT NOTES COMPUT SC, V3267, P18

[4]

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

[5]

Baresi L, 2002, LECT NOTES COMPUT SC, V2505, P402

[6] An Efficient Solution for Model Checking Graph Transformation Systems [J].

Baresi, Luciano ;

Rafe, Vahid ;

Rahmani, Adel T. ;

Spoletini, Paola .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 213 (01) :3-21

[7]

Ehrig H., 1999, Handbook of Graph Grammars and Computing by Graph Transformation: Applications, Languages and Tools, V2

[8]

Kastenberg H, 2006, LECT NOTES COMPUT SC, V3925, P299

[9] Towards Attributed Graphs in Groove [J].

Kastenberg, Harmen .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 154 (02) :47-54

[10]

KUSKE S, 2001, LECT NOTES COMPUTER, V2185

← 1 2 →