Adaptive Model Checking |
| |
Authors: | Groce Alex; Peled Doron; Yannakakis Mihalis |
| |
Institution: | Laboratory for Reliable Software, Jet Propulsion Laboratory, California Institute of Technology, Pasadena, CA 91109, USA. |
| |
Abstract: | We consider the case where inconsistencies are present betweena system and its corresponding model, used for automatic verification.Such inconsistencies can be the result of modeling errors orrecent 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 resultsto assist in automatically learning the required updates tothe model. In a related previous work, we have suggested theidea of black box checking, where verification starts withoutany model, and the model is obtained while repeated verificationattempts are performed. Under the current assumptions, an existinginaccurate (but not completely obsolete) model is used to expeditethe updates. We use techniques from black box testing and machinelearning. We present an implementation of the proposed methodologycalled AMC (for Adaptive Model Checking). We discuss some experimentalresults, comparing various tactics of updating a model whiletrying to perform model checking. |
| |
Keywords: | Black box testing learning regular languages model checking |
本文献已被 Oxford 等数据库收录! |
|