An algorithm for explanation counterexamples by use of a genetic algorithm

被引：0
|
作者：
Li Y. [1 ]
Huang S. [1 ]
Li Y. [1 ]
Chi R. [1 ]
Lang D. [1 ]
机构：
[1] College of Computer Science and Technology, Harbin Engineering University, Harbin
来源：
Harbin Gongcheng Daxue Xuebao/Journal of Harbin Engineering University | 2016年 / 37卷 / 10期
关键词：
Explanationing counterexample; Fault localization; Formal method; Genetic algorithm; Model checking;
D O I：
10.11990/jheu.201509006
中图分类号：
学科分类号：
摘要：
In order to seek the appropriate witness to help fault location of a complex system, a counterexample understanding algorithm in combination with a model checking technique on the basis of a genetic algorithm was proposed. The model used for model checking has an initial state, and the transfer relationship exists between the corresponding states. Therefore, a population was initialized. Also, a fitness function was designed and a directive mutation operation was conducted. Experimental results demonstrate that the algorithm can find the nearest witness rapidly and effectively and help the counterexample understanding of model checking. © 2016, Editorial Department of Journal of HEU. All right reserved.
引用
收藏
页码：1394 / 1399and1437
相关论文
共 21 条
  • [1] Clarke E., Grumberg O., Model Checking, (1999)
  • [2] Beer I., Ben-David S., Chockler H., Et al., Explaining counterexamples using causality, Formal Methods In System Design, 40, 1, pp. 20-40, (2012)
  • [3] Wang C., Yang Z., Ivancicf, Et al., Whodunit? Causal Analysis for Counterexamples, pp. 82-95, (2006)
  • [4] Huang H., Huang S., Chen Z., Et al., Understanding counterexamples based on Craig interpolation, Journal Of Jilin University: Science Edition, 51, 1, pp. 94-100, (2013)
  • [5] Halpern J.Y., Pearl J., Causes and explanations: a structural-model approach. Part I: Causes, British Journal For The Philosophy Of Science, 56, 4, pp. 843-887, (2005)
  • [6] Sulflow A., Fey G., Bloem R., Et al., Using unsatisfiable cores to debug multiple design errors, Proceedings of the 18th ACM Great Lakes symposium on VLSI, pp. 77-82, (2008)
  • [7] Chen Y., Safarpour S., Marques-Silva J., Et al., Automated design debugging with maximum satisfiability, IEEE Transactions On Computer-Aided Design Of Integrated Circuits And Systems, 29, 11, pp. 1804-1817, (2010)
  • [8] Groce A., Visser W., What Went Wrong: Explaining Coun-Terexamples, (2003)
  • [9] Groce A., Chaki S., Kroening D., Et al., Error explanation with distance metrics, International Journal On Software Tools For Technology Transfer, 8, 3, pp. 229-247, (2006)
  • [10] Chaki S., Groce A., Strichman O., Explaining abstract counterexamples, Proceedings of the 12th International Symposium on Foundations of Software Engineering, pp. 73-82, (2004)
123