Parameterized Verification of Systems with Global Synchronization and Guards

被引：7

作者：

Jaber, Nouraldin ^{[1
]}

Jacobs, Swen ^{[2
]}

Wagner, Christopher ^{[1
]}

Kulkarni, Milind ^{[1
]}

Samanta, Roopsha ^{[1
]}

机构：

[1] Purdue Univ, W Lafayette, IN 47907 USA

[2] CISPA Helmholtz Ctr Informat Secur, Saarbrucken, Germany

来源：

COMPUTER AIDED VERIFICATION (CAV 2020), PT I | 2020年 / 12224卷

基金：

美国国家科学基金会;

关键词：

MODEL CHECKING; SYMMETRY;

D O I：

10.1007/978-3-030-53288-8_15

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Inspired by distributed applications that use consensus or other agreement protocols for global coordination, we define a new computational model for parameterized systems that is based on a general global synchronization primitive and allows for global transition guards. Our model generalizes many existing models in the literature, including broadcast protocols and guarded protocols. We show that reachability properties are decidable for systems without guards, and give sufficient conditions under which they remain decidable in the presence of guards. Furthermore, we investigate cutoffs for reachability properties and provide sufficient conditions for small cutoffs in a number of cases that are inspired by our target applications.

引用

页码：299 / 323

页数：25

共 50 条

[1] Parameterized verification of π-calculus systems
Yang, Ping
Basu, Samik
Ramakrishnan, C. R.
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2006, 3920 : 42 - 57
[2] Verification of parameterized timed systems
Abdulla, PA
FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2005, 3829 : 95 - 97
[3] Parameterized Verification of Synchronization in Constrained Reconfigurable Broadcast Networks
Balasubramanian, A. R.
Bertrand, Nathalie
Markey, Nicolas
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2018, PT II, 2018, 10806 : 38 - 54
[4] Parameterized verification of monotone information systems
Chane-Yack-Fa, Raphael
Frappier, Marc
Mammar, Amel
Finkel, Alain
FORMAL ASPECTS OF COMPUTING, 2018, 30 (3-4) : 463 - 489
[5] Compositional analysis for verification of parameterized systems
Basu, S
Ramakrishnan, CR
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2003, 2619 : 315 - 330
[6] Compositional analysis for verification of parameterized systems
Basu, S
Ramakrishnan, CR
THEORETICAL COMPUTER SCIENCE, 2006, 354 (02) : 211 - 229
[7] Automatic abstraction for verification of parameterized systems
Zhang, Long
Qu, Wanxia
Guo, Yang
Li, Sikun
Jisuanji Fuzhu Sheji Yu Tuxingxue Xuebao/Journal of Computer-Aided Design and Computer Graphics, 2014, 26 (06): : 991 - 998
[8] Universal properties verification of parameterized parallel systems
Nugraheni, CE
COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2005, PT 3, 2005, 3482 : 453 - 462
[9] Incremental Inductive Verification of Parameterized Timed Systems
Isenberg, Tobias
2015 15TH INTERNATIONAL CONFERENCE ON APPLICATIONS OF CONCURRENCY TO SYSTEM DESIGN (ACSD), 2015, : 1 - 9
[10] An approach to the verification of symmetric parameterized distributed systems
Konnov, IV
Zakharov, VA
PROGRAMMING AND COMPUTER SOFTWARE, 2005, 31 (05) : 225 - 236

← 1 2 3 4 5 →