Model checking: Verification or debugging?

被引：0

作者：

Ruys, TC ^{[1
]}

Brinksma, E ^{[1
]}

机构：

[1] Univ Twente, Fac Comp Sci, NL-7500 AE Enschede, Netherlands

来源：

PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS I-V | 2000年

关键词：

model checking; verification; debugging;

D O I：

暂无

中图分类号：

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

学科分类号：

0812 ;

摘要：

Model checking tools are increasingly being used for the validation of real-life systems in an industrial context. This paper discusses two validation approaches with respect to the application of model checkers. The verification approach tries to ascertain the correctness of a formal model of a system, whereas the debugging approach tries to End errors in the model. This paper discusses the differences between the two complementing approaches and shows for each approach its advantages and disadvantages.

引用

页码：3009 / 3015

页数：7

共 50 条

[1] Model Checking: Algorithmic Verification and Debugging
Clarke, Edmund M.
Emerson, E. Allen
Sifakis, Joseph
COMMUNICATIONS OF THE ACM, 2009, 52 (11) : 75 - 84
[2] Model checking, testing and debugging
Hierons, Robert M.
Xie, Tao
SOFTWARE TESTING VERIFICATION & RELIABILITY, 2022, 32 (01):
[3] Contradictory Antecedent Debugging in Bounded Model Checking
Grosse, Daniel
Wille, Robert
Kuehne, Ulrich
Drechsler, Rolf
GLSVLSI 2009: PROCEEDINGS OF THE 2009 GREAT LAKES SYMPOSIUM ON VLSI, 2009, : 173 - 176
[4] A Practical Study of Debugging using Model Checking
Ogawa, Hideto
Ichii, Makoto
Kumeno, Fumihiko
Aoki, Toshiaki
2013 20TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2013), VOL 2, 2013, : 134 - 139
[5] A Method for Debugging of Pipe lined Processors in Formal Verification by Correspondence Checking
Velev, Miroslav N.
Gao, Ping
2010 15TH ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE (ASP-DAC 2010), 2010, : 608 - 613
[6] Design verification by model checking
1600, Japan Society for Software Science and Technology (31):
[7] MODEL CHECKING AND MODULAR VERIFICATION
GRUMBERG, O
LONG, DE
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (03): : 843 - 871
[8] Bytecode verification by model checking
ETH Zürich, Zürich, Switzerland
不详
不详
Basin, D., 1600, Kluwer Academic Publishers (30): : 3 - 4
[9] Bytecode Verification by Model Checking
David Basin
Stefan Friedrich
Marek Gawkowski
Journal of Automated Reasoning, 2003, 30 : 399 - 444
[10] MODEL CHECKING AND MODULAR VERIFICATION
GRUMBERG, O
LONG, DE
LECTURE NOTES IN COMPUTER SCIENCE, 1991, 527 : 250 - 265

← 1 2 3 4 5 →