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 条

[41] Formal Verification of 802.11 MAC Layer Handoff Process Using SPIN Model Checker
Zhao, Dan
Zhang, Dafang
Miao, Li
2009 WRI WORLD CONGRESS ON SOFTWARE ENGINEERING, VOL 3, PROCEEDINGS, 2009, : 402 - +
[42] Formal verification of ad-hoc routing protocols using SPIN model checker
de Renesse, R
Aghvami, AH
MELECON 2004: PROCEEDINGS OF THE 12TH IEEE MEDITERRANEAN ELECTROTECHNICAL CONFERENCE, VOLS 1-3, 2004, : 1177 - 1182
[43] Modeling and Verification of Timed Automaton Based Hybrid Systems Using Spin Model Checker
Kumar, Suresh N.
Kumar, G. Santhosh
2016 IEEE ANNUAL INDIA CONFERENCE (INDICON), 2016,
[44] Formal verification of a pipelined processor with new memory hierarchy using a commercial model checker
Nakamura, H
Arai, T
Fujita, M
2002 PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING, PROCEEDINGS, 2002, : 321 - 324
[45] MCMAS: an open-source model checker for the verification of multi-agent systems
Alessio Lomuscio
Hongyang Qu
Franco Raimondi
International Journal on Software Tools for Technology Transfer, 2017, 19 : 9 - 30
[46] Formal Verification of DEV&DESS Formalism Using Symbolic Model Checker HyTech
Choi, Han
Cha, Sungdeok
Jo, Jae Yeon
Yoo, Junbeom
Lee, Hae Young
Kim, Won-Tae
CONTROL AND AUTOMATION, AND ENERGY SYSTEM ENGINEERING, 2011, 256 : 112 - +
[47] MCMAS: an open-source model checker for the verification of multi-agent systems
Lomuscio, Alessio
Qu, Hongyang
Raimondi, Franco
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2017, 19 (01) : 9 - 30
[48] AUTOMATIC MODEL VERIFICATION FOR SEMICONDUCTOR MANUFACTURING SIMULATION
Gan, Boon Ping
Lendermann, Peter
Scholl, Wolfgang
Mosinski, Marcin
Preuss, Patrick
2013 WINTER SIMULATION CONFERENCE (WSC), 2013, : 3858 - 3865
[49] Automatic Verification of the Conceptual Model and Its Documentation
Laukaitis, Algirdas
Vasilecas, Olegas
BALTIC JOURNAL OF MODERN COMPUTING, 2009, 751 : 40 - 51
[50] Automatic memory reductions for RTL model verification
Manolios, Panagiotis
Srinivasan, Sudarshan K.
Vroon, Daron
IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN, DIGEST OF TECHNICAL PAPERS, ICCAD, 2006, : 40 - +

← 1 2 3 4 5 →