Forward reachability analysis of timed Petri nets

被引：0

作者：

Abdulla, PA ^{[1
]}

Deneux, J ^{[1
]}

Mahata, P ^{[1
]}

Nylén, A ^{[1
]}

机构：

[1] Uppsala Univ, Uppsala, Sweden

来源：

FORMAL TECHNIQUES, MODELLING AND ANALYSIS OF TIMED AND FAULT-TOLERANT SYSTEMS, PROCEEDINGS | 2004年 / 3253卷

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We consider verification of safety properties for concurrent real-timed systems modelled as timed Petri nets, by performing symbolic forward reachability analysis. We introduce a formalism, called region generators for representing sets of markings of timed Petri nets. Region generators characterize downward closed sets of regions, and provide exact abstractions of sets of reachable states with respect to safety properties. We show that the standard operations needed for performing symbolic reachability analysis are computable for region generators. Since forward reachability analysis is necessarily incomplete, we introduce an acceleration technique to make the procedure terminate more often on practical examples. We have implemented a prototype for analyzing timed Petri nets and used it to verify a parameterized version of Fischer's protocol and a producer-consumer protocol. We also used the tool to extract finite-state abstractions of these protocols.

引用

页码：343 / 362

页数：20

共 20 条

[1]

Abdulla PA, 1998, LECT NOTES COMPUT SC, V1427, P305, DOI 10.1007/BFb0028754

[2] Algorithmic analysis of programs with well quasi-ordered domains [J].

Abdulla, PA ;

Cerans, K ;

Jonsson, B ;

Tsay, YK .

INFORMATION AND COMPUTATION, 2000, 160 (1-2) :109-127

[3]

ABDULLA PA, 2001, LECT NOTES COMPUTER, V2075, P53, DOI DOI 10.1007/3-540-45740-2_

[4]

ABDULLA PA, 2003, 2003056 UPPS U DEP I

[5]

ALUR R, 1990, LECT NOTES COMPUT SC, V443, P322, DOI 10.1007/BFb0032042

[6]

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

[7]

BOUAJJANI A, 1997, LNCS, V1256

[8]

BOWDEN FDJ, 1996, P 2 AUSTR JAP WORKS

[9]

CLEAVELAND R, 1989, PROTOCOL SPECIFICATI, V9, P287

[10]

Delzanno G, 2000, LECT NOTES COMPUT SC, V1785, P426

← 1 2 →