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 条

[41] Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors
Charvat, Lukas
Smrcka, Ales
Vojnar, Tomas
2014 15TH INTERNATIONAL MICROPROCESSOR TEST AND VERIFICATION WORKSHOP (MTV 2014), 2015, : 83 - 89
[42] Parameterized model checking of networks of timed automata with Boolean guards
Spalazzi, Luca
Spegni, Francesco
THEORETICAL COMPUTER SCIENCE, 2020, 813 : 248 - 269
[43] Behavioral Automata Composition for Automatic Topology Independent Verification of Parameterized Systems
Hanna, Youssef
Basu, Samik
Rajan, Hridesh
7TH JOINT MEETING OF THE EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND THE ACM SIGSOFT SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING, 2009, : 325 - 334
[44] Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
Eichler, Paul
Jacobs, Swen
Weil-Kennedy, Chana
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2025, PT I, 2025, 15529 : 101 - 124
[45] Synchronization and anti-synchronization in global coupling chaotic systems
College of Physics Science, Shenzhen University, Shenzhen 518060, China
不详
Shenzhen Daxue Xuebao (Ligong Ban), 2008, 4 (422-426):
[46] Environment abstraction for parameterized verification
Clarke, E
Talupur, M
Veith, H
VERIFICATION, MODEL CHECKING , AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2006, 3855 : 126 - 141
[47] Monotonic Abstraction in Parameterized Verification
Abdulla, Parosh Aziz
Delzanno, Giorgio
Rezine, Ahmed
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 223 (0C) : 3 - 14
[48] Automated Parameterized Verification of CRDTs
Nagar, Kartik
Jagannathan, Suresh
COMPUTER AIDED VERIFICATION, CAV 2019, PT II, 2019, 11562 : 459 - 477
[49] Parameterized verification by probabilistic abstraction
Arons, T
Pnueli, A
Zuck, L
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2003, 2620 : 87 - 102
[50] Parameterized Verification of Transactional Memories
Emmi, Michael
Majumdar, Rupak
Manevich, Roman
PLDI '10: PROCEEDINGS OF THE 2010 ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2010, : 134 - 145

← 1 2 3 4 5 →