Verifying temporal properties of reactive systems:: A STeP tutorial

被引：35

作者：

Bjorner, NS ^{[1
]}

Browne, A ^{[1
]}

Colón, MA ^{[1
]}

Finkbeiner, B ^{[1
]}

Manna, Z ^{[1
]}

Sipma, HB ^{[1
]}

Uribe, TE ^{[1
]}

机构：

[1] Stanford Univ, Dept Comp Sci, Stanford, CA 94305 USA

来源：

FORMAL METHODS IN SYSTEM DESIGN | 2000年 / 16卷 / 03期

基金：

美国国家科学基金会; 美国国家航空航天局;

关键词：

temporal logic; deductive verification; verification diagrams; model checking;

D O I：

10.1023/A:1008700623084

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We review a number of formal verification techniques supported by STeP, the Stanford Temporal Prover, describing how the tool can be used to verify properties of several versions of the Bakery Mutual exclusion algorithm for mutual exclusion. We verify the classic two-process algorithm and simple variants, as well as an atomic parameterized version. The methods used include deductive verification rules, verification diagrams, automatic invariant generation, and finite-state model checking and abstraction.

引用

页码：227 / 270

页数：44

共 64 条

[1]

ALUR R, 1996, LNCS, V1102

[2]

[Anonymous], LECT NOTES COMPUTER

[3]

[Anonymous], LNCS

[4]

[Anonymous], THESIS EINDHOVEN U T

[5]

[Anonymous], THESIS STANFORD U

[6]

Barrett C, 1996, LECT NOTES COMPUT SC, V1166, P187, DOI 10.1007/BFb0031808

[7]

Bensalem S, 1998, LECT NOTES COMPUT SC, V1427, P319, DOI 10.1007/BFb0028755

[8]

BENSALEM S, 1996, LECT NOTES COMPUTER, V1102, P323

[9] Automatic generation of invariants and intermediate assertions [J].

Bjorner, N ;

Browne, A ;

Manna, Z .

THEORETICAL COMPUTER SCIENCE, 1997, 173 (01) :49-87

[10]

Bjorner NS, 1997, LECT NOTES ARTIF INT, V1249, P101

← 1 2 3 4 5 6 7 →