Adaptive model checking

Alex Groce, Doron Peled, Mihalis Yannakakis

Research output: Contribution to journalArticlepeer-review

31 Scopus citations

Abstract

We consider the case where inconsistencies are present between a system and its corresponding model, used for automatic verification. Such inconsistencies can be the result of modeling errors or recent modifications of the system. Despite such discrepancies, we can still attempt to perform automatic verification. In fact, as we show, we can sometimes exploit the verification results to assist in automatically learning the required updates to the model. In a related previous work, we have suggested the idea of black box checking, where verification starts without any model, and the model is obtained while repeated verification attempts are performed. Under the current assumptions, an existing inaccurate (but not completely obsolete) model is used to expedite the updates. We use techniques from black box testing and machine learning. We present an implementation of the proposed methodology called AMC (for Adaptive Model Checking). We discuss some experimental results, comparing various tactics of updating a model while trying to perform model checking.

Original languageEnglish (US)
Pages (from-to)729-744
Number of pages16
JournalLogic Journal of the IGPL
Volume14
Issue number5
DOIs
StatePublished - Oct 2006
Externally publishedYes

Keywords

  • Black box testing
  • Learning regular languages
  • Model checking

ASJC Scopus subject areas

  • Philosophy

Fingerprint

Dive into the research topics of 'Adaptive model checking'. Together they form a unique fingerprint.

Cite this