Automatic verification of a model checker by reflection

被引：0

作者：

Wang, BY ^{[1
]}

机构：

[1] Acad Sinica, Inst Informat Sci, Taipei 115, Taiwan

来源：

PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES | 2006年 / 3819卷

关键词：

reflection; rewriting logic; model checking; logic programming;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Intuitively, reflection is the feature that can represent and reason meta-level entities at the object level. In this paper, we use a reflective language to implement a local model checker and analyze the implementation. The implementation is greatly simplified by reflection. Further, we show the feature can be applied to verify the concise implementation rather easily. The simplicity of our approach suggests that reflection may be useful in the implementation and verification of other explicit-state model checking algorithms.

引用

下载

页码：45 / 59

页数：15

共 50 条

[21] YASM: A software model-checker for verification and refutation (Tool paper)
Gurfinkel, Arie
Wei, Ou
Chechik, Marsha
COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2006, 4144 : 170 - 174
[22] Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
Julian Brunner
Peter Lammich
Journal of Automated Reasoning, 2018, 60 : 3 - 21
[23] Verification of Multi Decisional Reactive Agent using SMV Model Checker
Haqiq, Abdelhay
Bounabat, Bouchaib
2013 8TH INTERNATIONAL DESIGN AND TEST SYMPOSIUM (IDT), 2013,
[24] Modelling and Verification of the FlexRay Startup Mechanism using UPPAAL Model Checker
Asokan, Shimmi
SanthoshKumar, G.
PROCEEDINGS OF THE 2018 8TH INTERNATIONAL SYMPOSIUM ON EMBEDDED COMPUTING AND SYSTEM DESIGN (ISED 2018), 2018, : 69 - 73
[25] Efficiency of formal verification of ArchiMate business processes with NuSMV model checker
Szwed, Piotr
PROCEEDINGS OF THE 2015 FEDERATED CONFERENCE ON COMPUTER SCIENCE AND INFORMATION SYSTEMS, 2015, 5 : 1427 - 1436
[26] Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
Brunner, Julian
Lammich, Peter
NASA FORMAL METHODS, NFM 2016, 2016, 9690 : 307 - 321
[27] Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker
Conchon, Sylvain
Delzanno, Giorgio
Ferrando, Angelo
FUNDAMENTA INFORMATICAE, 2021, 178 (04) : 347 - 378
[28] MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
Cermak, Petr
Lomuscio, Alessio
Mogavero, Fabio
Murano, Aniello
COMPUTER AIDED VERIFICATION, CAV 2014, 2014, 8559 : 525 - 532
[29] Interlocking control by Distributed Signal Boxes: Design and verification with the SPIN model checker
Basagiannis, Stylianos
Katsaros, Panagiotis
Pombortsis, Andrew
PARALLEL AND DISTRIBUTED PROCESSING AND APPLICATIONS, 2006, 4330 : 317 - +
[30] Modelling and Verification of CoAP over Routing Layer using SPIN Model Checker
Vattakunnel, Anchal J.
Kumar, Suresh N.
Kumar, G. Santhosh
PROCEEDINGS OF THE 6TH INTERNATIONAL CONFERENCE ON ADVANCES IN COMPUTING AND COMMUNICATIONS, 2016, 93 : 299 - 308

← 1 2 3 4 5 →