State Identification for Labeled Transition Systems with Inputs and Outputs
- 26 Downloads
For Finite State Machines (FSMs) a rich testing theory has been developed to discover aspects of their behavior and ensure their correct functioning. Although this theory is widely used, e.g., to check conformance of protocol implementations, its applicability is limited by restrictions of the FSM framework: the fact that inputs and outputs alternate in an FSM, and outputs are fully determined by the previous input and state. Labeled Transition Systems with inputs and outputs (LTSs), as studied in ioco testing theory, provide a richer framework for testing component oriented systems, but lack the algorithms for test generation from FSM theory.
In this article, we propose an algorithm for the fundamental problem of state identification during testing of LTSs. Our algorithm is a direct generalization of the well-known algorithm for computing adaptive distinguishing sequences for FSMs proposed by Lee & Yannakakis. Our algorithm has to deal with so-called compatible states, states that cannot be distinguished in case of an adversarial system-under-test. Analogous to the result of Lee & Yannakakis, we prove that if an (adaptive) test exists that distinguishes all pairs of incompatible states of an LTS, our algorithm will find one. In practice, such adaptive tests typically do not exist. However, in experiments with an implementation of our algorithm on an industrial benchmark, we find that tests produced by our algorithm still distinguish more than 99% of the incompatible state pairs.
- 1.Alur, R., Courcoubetis, C., Yannakakis, M.: Distinguishing tests for nondeterministic and probabilistic machines. In: STOC, vol. 95, pp. 363–372. Citeseer (1995)Google Scholar
- 3.Beneš, N., Daca, P., Henzinger, T.A., Křetínskỳ, J., Ničković, D.: Complete composition operators for IOCO-testing theory. In: Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering. CBSE 2015, pp. 101–110. ACM, New York (2015). https://doi.org/10.1145/2737166.2737175
- 4.van den Bos, P., Vaandrager, F.W.: State identification for labeled transition systems with inputs and outputs. CoRR abs/1907.11034 (2019). http://arxiv.org/abs/1907.11034
- 6.van den Bos, P., Stoelinga, M.: Tester versus bug: a generic framework for model-based testing via games. In: Orlandini, A., Zimmermann, M. (eds.) Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification. Electronic Proceedings in Theoretical Computer Science, Saarbrücken, Germany, 26–28th September 2018, vol. 277, pp. 118–132. Open Publishing Association (2018). https://doi.org/10.4204/EPTCS.277.9
- 8.Dijkstra, E.W.: Guarded commands, nondeterminacy, and formal derivation of programs. In: Gries, D. (ed.) Programming Methodology: A Collection of Articles by Members of IFIP WG2.3. Texts and Monographs in Computer Science, pp. 166–175. Springer, New York (1978). https://doi.org/10.1007/978-1-4612-6315-9_14CrossRefGoogle Scholar
- 16.Moerman, J.: Nominal techniques and black box testing for automata learning. Ph.D. thesis, Radboud University Nijmegen, July 2019Google Scholar
- 17.Moore, E.F.: Gedanken-experiments on sequential machines. In: Annals of Mathematics Studies, vol. 34, pp. 129–153. Princeton University Press, Princeton (1956)Google Scholar
- 20.Bensalem, S., Krichen, M., Tripakis, S.: State identification problems for input/output transition systems. In: 2008 9th International Workshop on Discrete Event Systems, pp. 225–230, May 2008. https://doi.org/10.1109/WODES.2008.4605949
- 21.Simão, A., Petrenko, A.: Generating complete and finite test suite for ioco: is it possible? In: Proceedings Ninth Workshop on Model-Based Testing, MBT 2014, Grenoble, France, 6 April 2014, pp. 56–70 (2014). https://doi.org/10.4204/EPTCS.141.5
- 22.Smeenk, W.: Applying automata learning to complex industrial software. Master’s thesis, Radboud University Nijmegen (2012)Google Scholar