Adaptive model checking

Alex Groce, Doron Peled, Mihalis Yannakakis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

85 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)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 8th Int. Conf., TACAS 2002, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2002, Proc.
EditorsJoost-Pieter Katoen, Perdita Stevens
PublisherSpringer-Verlag
Pages357-370
Number of pages14
ISBN (Print)3540434194, 9783540434191
DOIs
StatePublished - 2002
Externally publishedYes
Event8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings - Grenoble, France
Duration: Apr 8 2002Apr 12 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2280 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings
Country/TerritoryFrance
CityGrenoble
Period4/8/024/12/02

Keywords

  • Automatic verification
  • Black box testing
  • Learning algorithms

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

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

Cite this