Abstract
There are many cases where we want to verify a system that does not have a usable formal model: the model may be missing, out of date, or simply too big to be used. A possible method is to analyze the system while learning the model (black box checking). However, learning may be an expensive task, thus it needs to be guided, e.g., using the checked property or an inaccurate model (adaptive model checking). In this paper, we consider the case where some of the system components are completely specified (white boxes), while others are unknown (black boxes), giving rise to a grey box system. We provide algorithms and lower bounds, as well as experimental results for this model.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Madhusudan, P., Nam, W.: Symbolic Compositional Verification by Learning Assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 548–562. Springer, Heidelberg (2005)
Angluin, D.: Learning Regular Sets from Queries and Counterexamples. Information and Computation 75, 87–106 (1987)
Alur, R., Grosu, R., McDougall, M.: Efficient Reachability Analysis of Hierarchical Reactive Machines. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 280–295. Springer, Heidelberg (2000)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E., Long, D., McMillan, K.: Compositional Model Checking. In: LICS 1989, pp. 353–362. IEEE, Los Alamitos (1989)
Chow, T.S.: Testing software design modeled by finite-states machines. IEEE transactions on software engineering SE-4, 178–187 (1978)
Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Elkind, E., Genest, B., Peled, D., Qu, H.: Grey-Box Checking. Internal Report, Available at: http://www.crans.org/~genest/EGPQ.ps
Groce, A., Peled, D.A., Yannakakis, M.: Adaptive Model Checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 357–370. Springer, Heidelberg (2002)
Mazurkiewicz, A.: Trace Semantics. In: Honnef, B. Proceedings of Advances in Petri Nets, 1986. LNCS, pp. 279–324. Springer, Heidelberg (1987)
Ochmanski, E.: Languages and Automata. In: Diekert, V., Rozenberg, G. (eds.) The Book of Traces, pp. 167–204. World Scientific, Singapore
Peled, D., Vardi, M., Yannakakis, M.: Black Box Checking. In: FORTE/PSTV 1999 (1999)
Rivest, R., Schapire, R.: Inference of Finite Automata Using Homing Sequences. Information and Computation 103(2), 299–347 (1993)
Vasilevskii, M.P.: Failure diagnosis of automata. Kibertetika 4, 98–108 (1973)
Weimer, W., Necula, G.C.: Mining Temporal Specifications for Error Detection. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 461–476. Springer, Heidelberg (2005)
Xie, G., Dang, Z.: Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach. In: Grieskamp, W., Weise, C. (eds.) FATES 2005. LNCS, vol. 3997, pp. 170–186. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Elkind, E., Genest, B., Peled, D., Qu, H. (2006). Grey-Box Checking. In: Najm, E., Pradat-Peyre, JF., Donzeau-Gouge, V.V. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2006. FORTE 2006. Lecture Notes in Computer Science, vol 4229. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11888116_30
Download citation
DOI: https://doi.org/10.1007/11888116_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-46219-4
Online ISBN: 978-3-540-46220-0
eBook Packages: Computer ScienceComputer Science (R0)