Verification of Concurrent Programs Using Petri Net Unfoldings

被引：6

作者：

Dietsch, Daniel ^{[1
]}

Heizmann, Matthias ^{[1
]}

Klumpp, Dominik ^{[1
]}

Naouar, Mehdi ^{[1
]}

Podelski, Andreas ^{[1
]}

Schaetzle, Claus ^{[1
]}

机构：

[1] Univ Freiburg, Freiburg, Germany

来源：

VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2021 | 2021年 / 12597卷

关键词：

Petri nets; Unfoldings; Concurrency; Verification;

D O I：

10.1007/978-3-030-67067-2_9

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Given a verification problem for a concurrent program (with a fixed number of threads) over infinite data domains, we can construct a model checking problem for an abstraction of the concurrent program through a Petri net (a problem which can be solved using McMillan's unfoldings technique). We present a method of abstraction refinement which translates Floyd/Hoare-style proofs for sample traces into additional synchronization constraints for the Petri net.

引用

页码：174 / 195

页数：22

共 50 条

[21] Identifying state coding conflicts in asynchronous system specifications using Petri net unfoldings
Kondratyev, A
Cortadella, J
Kishinevsky, M
Lavagno, L
Taubin, A
Yakovlev, A
1998 INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 1998, : 152 - 163
[22] Modular Construction of Finite and Complete Prefixes of Petri net Unfoldings
Madalinski, Agnes
Fabre, Eric
FUNDAMENTA INFORMATICAE, 2009, 95 (01) : 219 - 244
[23] Modular construction of finite and complete prefixes of Petri net unfoldings
Madalinski, Agnes
Fabre, Eric
2008 8TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2008, : 68 - 77
[24] On the Verification of Non-autonomous Petri Net Models Using Autonomous Petri Net Tools
Barros, Joao Paulo
Gomes, Luis
Costa, Aniko
38TH ANNUAL CONFERENCE ON IEEE INDUSTRIAL ELECTRONICS SOCIETY (IECON 2012), 2012, : 6138 - 6143
[25] A graph theoretic approach to reachability problem with Petri net unfoldings
Miyamoto, T
Kumagai, S
IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1996, E79A (11) : 1809 - 1816
[26] Instruction list verification using a Petri net semantics
Heiner, M
Menzel, T
1998 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS, VOLS 1-5, 1998, : 716 - 721
[27] Integration of robotics components and verification using petri net
Srivastava, Ratnesh Prasad
Nandi, G. C.
2017 INTERNATIONAL CONFERENCE ON INNOVATIONS IN CONTROL, COMMUNICATION AND INFORMATION SYSTEMS (ICICCI-2017), 2017, : 80 - 86
[28] MODELLING AND VERIFICATION OF CONCURRENT PROGRAMS USING UPPAAL
Cicirelli, Franco
Nigro, Libero
Pupo, Francesco
PROCEEDINGS - 25TH EUROPEAN CONFERENCE ON MODELLING AND SIMULATION, ECMS 2011, 2011, : 525 - 533
[29] Synthesis of next state feedback control of discrete event systems by using Petri net unfoldings
Miyamoto, T
Kumagai, S
SICE 2004 ANNUAL CONFERENCE, VOLS 1-3, 2004, : 2074 - 2079
[30] Enforcing Periodic Transition Deadlines in Time Petri Nets With Net Unfoldings
Wang, Haisheng
Grigore, Liviu
Buy, Ugo
Lehene, Mihai
Darabi, Houshang
IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2011, 41 (03): : 522 - 539

← 1 2 3 4 5 →