Trio2Promela: a model checker for temporal metric specifications

被引：5

作者：

Bianculli, Domenico ^{[1
]}

Morzenti, Angelo ^{[2
]}

Pradella, Matteo ^{[3
]}

Pietro, Pierluigi San ^{[2
]}

Spoletini, Paola ^{[2
]}

机构：

[1] Univ Lugano, Fac Informat, Lugano, Switzerland

[2] Politecn Milan, Dipartimento Elettron & Informaz, Milan, Italy

[3] CNR, IEIIT MI, I-00185 Rome, Italy

来源：

29TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: ICSE 2007 COMPANION VOLUME, PROCEEDINGS | 2007年

关键词：

LOGIC; SPIN;

D O I：

10.1109/ICSECOMPANION.2007.79

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We present Trio2Promela, a tool for model checking metric temporal logic specifications written in the TRIO language. Our approach is based on the translation of formulae into Promela programs for the model checker Spin, guided by equivalence between temporal logic and alternating Buchi automata. Trio2Promela may be used also to check satisfiability of temporal logic specifications (a distinguishing difference with other model checking tools).

引用

页码：61 / +

页数：2

共 10 条

[1]

BIANCULLI D, 2007, FSEN 07 P INT S FUND

[2] Automated deductive requirements analysis of critical systems [J].

Gargantini, A ;

Morzenti, A .

ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2001, 10 (03) :255-307

[3]

Gastin P, 2001, LECT NOTES COMPUT SC, V2102, P53

[4] The model checker SPIN [J].

Holzmann, GJ .

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

[5]

KUPFERMAN O, 1997, ISTCS, P147

[6] GENERATING TEST CASES FOR REAL-TIME SYSTEMS FROM LOGIC SPECIFICATIONS [J].

MANDRIOLI, D ;

MORASCA, S ;

MORZENTI, A .

ACM TRANSACTIONS ON COMPUTER SYSTEMS, 1995, 13 (04) :365-398

[7] A MODEL PARAMETRIC REAL-TIME LOGIC [J].

MORZENTI, A ;

MANDRIOLI, D ;

GHEZZI, C .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1992, 14 (04) :521-573

[8]

Morzenti A, 2003, LECT NOTES COMPUT SC, V2805, P542

[9]

PRADELLA M, 2003, ATVA03 1 WORKSH AUT

[10]

Somenzi F., 2000, LNCS, V1855, P248, DOI [10.1007/10722167_21, DOI 10.1007/10722167_21, DOI 10.1007/1072216721]

← 1 →