TY - GEN
T1 - Adaptive model checking
AU - Groce, Alex
AU - Peled, Doron
AU - Yannakakis, Mihalis
PY - 2002
Y1 - 2002
N2 - 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.
AB - 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.
KW - Automatic verification
KW - Black box testing
KW - Learning algorithms
UR - http://www.scopus.com/inward/record.url?scp=84888270231&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84888270231&partnerID=8YFLogxK
U2 - 10.1007/3-540-46002-0_25
DO - 10.1007/3-540-46002-0_25
M3 - Conference contribution
AN - SCOPUS:84888270231
SN - 3540434194
SN - 9783540434191
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 357
EP - 370
BT - Tools 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.
A2 - Katoen, Joost-Pieter
A2 - Stevens, Perdita
PB - Springer-Verlag
T2 - 8th 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
Y2 - 8 April 2002 through 12 April 2002
ER -