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 条

[41] Enhancing model checking in verification by AI techniques
Buccafurri, F
Eiter, T
Gottlob, G
Leone, N
ARTIFICIAL INTELLIGENCE, 1999, 112 (1-2) : 57 - 104
[42] Analog Circuit Verification by Statistical Model Checking
Wang, Ying-Chih
Komuravelli, Anvesh
Zuliani, Paolo
Clarke, Edmund M.
2011 16TH ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE (ASP-DAC), 2011,
[43] Diagnosability verification using LTL model checking
Tuxi, Thiago M.
Carvalho, Lilian K.
Nunes, Eduardo V. L.
da Cunha, Antonio E. C.
DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2022, 32 (03): : 399 - 433
[44] Verification of ACTL properties by bounded model checking
Zhang, Wenhui
COMPUTER AIDED SYSTEMS THEORY- EUROCAST 2007, 2007, 4739 : 556 - 563
[45] Verification of ArchiMate Behavioral Elements by Model Checking
Szwed, Piotr
COMPUTER INFORMATION SYSTEMS AND INDUSTRIAL MANAGEMENT, 2015, 9339 : 132 - 144
[46] Formal Verification of Mobile Orchestration Agents Model checking for orchestration verification
Mahmoudi, Charif
Mourlin, Fabrice
2017 INTERNATIONAL CONFERENCE ON WIRELESS TECHNOLOGIES, EMBEDDED AND INTELLIGENT SYSTEMS (WITS), 2017,
[47] Verification method of security model based on UML and model checking
Cheng, Liang
Zhang, Yang
Jisuanji Xuebao/Chinese Journal of Computers, 2009, 32 (04): : 699 - 708
[48] Enhanced Design Debugging With Assistance From Guidance-Based Model Checking
Vineesh, V. S.
Kumar, Binod
Shinde, Rushikesh
Sharma, Neelam
Fujita, Masahiro
Singh, Virendra
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2021, 40 (05) : 985 - 998
[49] Debugging Smart Contract’s Business Logic Using Symbolic Model Checking
E. Shishkin
Programming and Computer Software, 2019, 45 : 590 - 599
[50] Debugging Smart Contract's Business Logic Using Symbolic Model Checking
Shishkin, E.
PROGRAMMING AND COMPUTER SOFTWARE, 2019, 45 (08) : 590 - 599

← 1 2 3 4 5 →