Dynamic State Space Partitioning for External Memory Model Checking

被引：0

作者：

Evangelista, Sami ^{[1
]}

Kristensen, Lars Michael ^{[2
]}

机构：

[1] Aarhus Univ, Dept Comp Sci, DK-8000 Aarhus C, Denmark

[2] Univ Bergen, Dept Comp Engn, N-5020 Bergen, Norway

来源：

FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS | 2009年 / 5825卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We describe a dynamic partitioning scheme usable by model checking techniques that divide the state space into partitions, such as most external memory and distributed model checking algorithms. The goal of the scheme is to reduce the number of transitions that link states belonging to different partitions, and thereby limit the amount of disk access and network communication. We report on several experiments made with our verification platform ASAP that implements the dynamic partitioning scheme proposed in this paper.

引用

页码：70 / +

页数：2

共 50 条

[21] Automatic timing model generation by CFG partitioning and model checking
Wenzel, I
Rieder, B
Kirner, R
Puschner, P
DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, VOLS 1 AND 2, PROCEEDINGS, 2005, : 606 - 611
[22] State space formulation for linear viscoelastic dynamic systems with memory
Palmeri, A
Ricciardelli, F
De Luca, A
Muscolino, G
JOURNAL OF ENGINEERING MECHANICS-ASCE, 2003, 129 (07): : 715 - 724
[23] Reordering Control Approaches to State Explosion in Model Checking with Memory Consistency Models
Abe, Tatsuya
Ugawa, Tomoharu
Maeda, Toshiyuki
VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS (VSTTE 2017), 2017, 10712 : 170 - 190
[24] Dynamic partitioning of shared cache memory
Suh, GE
Rudolph, L
Devadas, S
JOURNAL OF SUPERCOMPUTING, 2004, 28 (01): : 7 - 26
[25] Predictive State Representations with State Space Partitioning
Liu, Yunlong
Tang, Yun
Zeng, Yifeng
PROCEEDINGS OF THE 2015 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS (AAMAS'15), 2015, : 1259 - 1266
[26] Dynamic Partitioning of Shared Cache Memory
G. E. Suh
L. Rudolph
S. Devadas
The Journal of Supercomputing, 2004, 28 : 7 - 26
[27] Reducing State Explosion for Software Model Checking with Relaxed Memory Consistency Models
Abe, Tatsuya
Ugawa, Tomoharu
Maeda, Toshiyuki
Matsumoto, Kousuke
DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, 2016, 9984 : 118 - 135
[28] Using Decision Diagrams to Compactly Represent the State Space for Explicit Model Checking
Zheng, Hao
Price, Andrew
Myers, Chris
2012 IEEE INTERNATIONAL HIGH LEVEL DESIGN VALIDATION AND TEST WORKSHOP (HLDVT), 2012, : 17 - 24
[29] Attacking State Space Explosion Problem in Model Checking Embedded TV Software
Comert, Furkan
Ovatman, Tolga
IEEE TRANSACTIONS ON CONSUMER ELECTRONICS, 2015, 61 (04) : 572 - 580
[30] A Model Checking Method for Secure Routing Protocols by SPIN with State Space Reduction
Kojima, Hideharu
Yanai, Naoto
2020 IEEE 34TH INTERNATIONAL PARALLEL AND DISTRIBUTED PROCESSING SYMPOSIUM WORKSHOPS (IPDPSW 2020), 2020, : 627 - 635

← 1 2 3 4 5 →