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.
Chapter PDF
Similar content being viewed by others
References
D. Angluin, Learning Regular Sets from Queries and Counterexamples, Information and Computation, 75, 87–106 (1978).
G. Birtwistle, F. Moller, Ch. Tofts, The verification of a COMA cache coherence protocol, IEEE Workshop on Formal Methods in Software Practice (FMSP’96).
T. S. Chow, Testing software design modeled by finite-state machines, IEEE transactions on software engineering, SE-4, 3, 1978, 178–187.
E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement, CAV 2000, 154–169.
R. Cleaveland, J. Parrow, B. Steffen, The Concurrency Workbench: a semantic-based tool for the verification of concurrent systems, TOPLAS 15(1993), 36–72.
Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M., Memory efficient algorithms for the verification of temporal properties, Formal Methods in System Design 1(1992), pp. 275–288.
J.E. Hopcroft, An n log n algorithm for minimizing the states in infinite automata, The theory of Machines and Computation, Academic Press, New York, 189–196, 1971.
D. Lee, M. Yannakakis, Principles and methods of testing finite state machines—a survey, Proceedings of the IEEE, 84(8), 1090–1126, 1996.
D. Peled, M. Y. Vardi, M. Yannakakis, Black Box Checking, Black Box Checking, FORTE/PSTV 1999, Beijing, China.
M. P. Vasilevskii, Failure diagnosis of automata, Kibertetika, no 4, 1973, 98–108.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Groce, A., Peled, D., Yannakakis, M. (2002). Adaptive Model Checking. In: Katoen, JP., Stevens, P. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2002. Lecture Notes in Computer Science, vol 2280. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46002-0_25
Download citation
DOI: https://doi.org/10.1007/3-540-46002-0_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43419-1
Online ISBN: 978-3-540-46002-2
eBook Packages: Springer Book Archive