Abstract model checking and refinement of temporal logic in αSPIN

被引：0

作者：

Gallardo, MD ^{[1
]}

Martínez, J ^{[1
]}

Merino, P ^{[1
]}

Pimentel, E ^{[1
]}

机构：

[1] Univ Malaga, Dept Comp Sci, Malaga 29071, Spain

来源：

THIRD INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS | 2003年

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper gives an overview of the features offered by the tool alphaSPIN in order to perform abstract model checking of LTL formulas. Shortly, these features are: construction of over-approximated PROMELA models, checking satisfaction of universal formulas, checking refutation of existential formulas, and on-the-fly refinement of the model by means of a refinement of the temporal formula to be verified.

引用

页码：245 / 246

页数：2

共 9 条

[1]

Clarke Edmund, 2000, Computer Aided Verification, P154, DOI [10.1007/10722167_15, DOI 10.1007/10722167_15]

[2] MODEL CHECKING AND ABSTRACTION [J].

CLARKE, EM ;

GRUMBERG, O ;

LONG, DE .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (05) :1512-1542

[3]

CLEVELAND R, 1995, LNCS, V983, P51

[4] Abstract interpretation of reactive systems [J].

Dams, D ;

Gerth, R ;

Grumberg, O .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1997, 19 (02) :253-291

[5]

Gallardo MD, 2002, LECT NOTES COMPUT SC, V2477, P395

[6]

GALLARDO MM, 2002, FMICS 02 7 INT WORKS, V66

[7]

GALLARDO MM, 2002, WFLP 02 11 INT WORKS

[8]

Giacobazzi R, 2001, LECT NOTES COMPUT SC, V2126, P356

[9] The model checker SPIN [J].

Holzmann, GJ .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1997, 23 (05) :279-295

← 1 →