Abstract
Two main approaches are used for increasing the quality of systems: in model checking, one checks properties of a known design of a system; in testing, one usually checks whether a given implementation, whose internal structure is often unknown, conforms with an abstract design. We are interested in the combination of these techniques. Namely, we would like to be able to test whether an implementation with unknown structure satisfies some given properties. We propose and formalize this problem of black box checking and suggest several algorithms. Since the input to black box checking is not given initially, as is the case in the classical model of computation, but is learned through experiments, we propose a computational model based on games with incomplete information. We use this model to analyze the complexity of the problem. We also address the more practical question of finding an approach that can detect errors in the implementation before completing an exhaustive search.
Supported in part by NSF grants CCR-9628400 and CCR-9700061, and by a grant from the Intel Corporation. Part of this work was done when this author was a Varon Visiting Professor at the Weizmann Institute of Science.
Chapter PDF
Similar content being viewed by others
References
R. Alur, C. Courcoubetis, M. Yannakakis, Distinguishing tests for nondeterministic and probablistic machines, Symposium on Theory of Computer Science, 1995, ACM, 363–372.
D. Angluin, Learning Regular Sets from Queries and Counterexamples, Information and Computation, 75, 87–106 (1978).
J. R. Büchi, On a decision method in restricted second order arithmetic, Proceedings of International Congress on Logic, Methodology and Philosophy of Science, Palo Alto, CA, USA, 1960, 1–11.
T. S. Chow, Testing software design modeled by finite-state machines, IEEE transactions on software engineering, SE-4, 3, 1978, 178–187.
E.M. Clarke, O. Grumberg, D. Peled, Model Checking, MIT Press, to appear 1999.
R. Gerth, D. Peled, M. Vardi, P. Wolper, Simple on-the-fly automatic verification of linear temporal logic, Protocol Specification Testing and Verification, 1995, Chapman and Hall, 3–18, Warsaw, Poland.
P. Godefroid, Model checking for programming languages using VeriSoft, Proc. 24th ACM Symp. on Progr. Lang. and Sys., 174–186, 1996.
F. C. Hennie, Fault detecting experiments for sequential circuits, Proc. 5th Ann. Symp. Switching Circuit Theory and Logical Design, 95–110, 1964.
G. J. Holzmann, D. Peled, The State of Spin, 8th International Conference on Computer Aided Verification, Springer Verlag, LNCS, 1102, 385–389, 1996, New Brunswick, NJ, USA.
Z. Kohavi, Switching and Finite Automata Theory, 1978, McGraw Hill.
R. P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, Princeton University Press, 1995.
D. Lee, M. Yannakakis, Principles and methods of testing finite state machines–a survey, Proceedings of the IEEE, 84 (8), 1090–1126, 1996.
O. Maler, A. Pnueli, On the learnability of infinitary regular sets, Information and Computation 118 (1995), 316–326.
E. F. Moore, Gedanken-experiments on sequential machines, Automata Studies, Princeton University Press, 1956, 129–153.
G. J. Myers, The Art of Software Testing, Wiley International, 1979.
A. Pnueli, The temporal logic of programs, 18th IEEE symposium on Foundation of Computer Science, 1977, 46–57.
J.H. Reif, The complexity of two-player games of incomplete information, Journal of computer and system sciences, 29, 1984, 274–301.
R. L. Rivest, R. E. Schapire, Inference of finite automata using homing sequences, Information and Computation 103, 299–347, 1993.
D. P. Sidhu, T. K. Leung, Formal methods for protocol testing: a detailed study, IEEE Trans. Sw Eng., 15, 413–426, 1989.
W. Thomas, Automata on infinite objects, Handbook of Theoretical Computer Science, MIT Press, J. van Leeuwen (Ed.), 135–192.
B. A. Trakhtenbrot, Y. M. Barzdin, Finite Automata: Behavior and Synthesis, North Holland, 1973.
M. Y. Vardi, P. Wolper, An automata-theoretic approach to automatic program verification, Proceedings of the First Symposium on Logic in Computer Science, Cambridge, UK, 322–331.
M. P. Vasilevskii, Failure diagnosis of automata, Kibertetika, no 4, 1973, 98108.
M. Yannakakis, D. Lee, Testing finite state machines: fault detection, J. Computer and Syst. Sci., 50, 209–227, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Peled, D., Vardi, M.Y., Yannakakis, M. (1999). Black Box Checking. In: Wu, J., Chanson, S.T., Gao, Q. (eds) Formal Methods for Protocol Engineering and Distributed Systems. PSTV FORTE 1999 1999. IFIP Advances in Information and Communication Technology, vol 28. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35578-8_13
Download citation
DOI: https://doi.org/10.1007/978-0-387-35578-8_13
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5270-0
Online ISBN: 978-0-387-35578-8
eBook Packages: Springer Book Archive