首页|Automatic verification of reduction techniques in Higher Order Logic
Automatic verification of reduction techniques in Higher Order Logic
扫码查看
点击上方二维码区域，可以放大扫码查看
原文链接
NETL
NSTL
Springer Nature
In this paper we propose an automatic methodology to verify the soundness of model checking reduction techniques. The idea is to use the consistency of the specifications to verify if the reduced model is faithful to the original one. The user provides the reduction technique, the specification and the system under verification. Then, using Higher Order Logic he verifies automatically if the reduction technique is soundly applied. The method is completely defined in an MDG-HOL special integration platform that combines an automatic high level model checking tool Multiway Decision Graphs (MDGs) within the HOL theorem prover. We provide two case studies, the first one is the reduction using SAT-MDG of an Island Tunnel Controller and the second one is the MDG-HOL assume-guarantee reduction of the Look-Aside Interface. The obtained results of our approach offer a considerable gain in terms of the correctness of heuristics and reduction techniques as applied to commercial model checking, however a small penalty is paid in terms of CPU time and memory usage.
HOL theorem proverMultiway decision graphsReduction techniquesSoundness
Sa'ed Abed、Otmane Ait Mohamed、Ghiath Al Sammane
展开 >
Department of Computer Engineering, Hashemite University. Zarqa, Jordan
Department of Electrical and Computer Engineering, Concordia University. Montreal. Canada
NETL
NSTL
Springer Nature
