Abstract
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.
Funded by the Netherlands Organisation of Scientific Research (NWO) under project 13859: Supersizing Model-Based testing (SUMBAT).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Alur, R., Courcoubetis, C., Yannakakis, M.: Distinguishing tests for nondeterministic and probabilistic machines. In: STOC, vol. 95, pp. 363–372. Citeseer (1995)
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)
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
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
van den Bos, P., Janssen, R., Moerman, J.: n-complete test suites for IOCO. Softw. Qual. J. 27(2), 563–588 (2019). https://doi.org/10.1007/s11219-018-9422-x
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
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)
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_14
Dorofeeva, R., El-Fakih, K., Maag, S., Cavalli, A.R., Yevtushenko, N.: FSM-based conformance testing methods: a survey annotated with experimental evaluation. Inf. Softw. Technol. 52(12), 1286–1297 (2010)
Gill, A.: Introduction to the Theory of Finite-State Machines. McGraw-Hill, New York (1962)
Hierons, R.M.: Testing from a nondeterministic finite state machine using adaptive state counting. IEEE Trans. Comput. 53(10), 1330–1342 (2004). https://doi.org/10.1109/TC.2004.85
Lee, D., Yannakakis, M.: Testing finite-state machines: state identification and verification. IEEE Trans. Comput. 43(3), 306–320 (1994). https://doi.org/10.1109/12.272431
Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines – a survey. Proc. IEEE 84(8), 1090–1123 (1996)
Mazala, R.: Infinite games. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata Logics, and Infinite Games. LNCS, vol. 2500, pp. 23–38. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36387-4_2
Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)
Moerman, J.: Nominal techniques and black box testing for automata learning. Ph.D. thesis, Radboud University Nijmegen, July 2019
Moore, E.F.: Gedanken-experiments on sequential machines. In: Annals of Mathematics Studies, vol. 34, pp. 129–153. Princeton University Press, Princeton (1956)
Petrenko, A., Yevtushenko, N.: Conformance tests as checking experiments for partial nondeterministic FSM. In: Grieskamp, W., Weise, C. (eds.) FATES 2005. LNCS, vol. 3997, pp. 118–133. Springer, Heidelberg (2006). https://doi.org/10.1007/11759744_9
Petrenko, A., Yevtushenko, N.: Adaptive testing of deterministic implementations specified by nondeterministic FSMs. In: Wolff, B., Zaïdi, F. (eds.) ICTSS 2011. LNCS, vol. 7019, pp. 162–178. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24580-0_12
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
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
Smeenk, W.: Applying automata learning to complex industrial software. Master’s thesis, Radboud University Nijmegen (2012)
Smeenk, W., Moerman, J., Vaandrager, F., Jansen, D.N.: Applying automata learning to embedded control software. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 67–83. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25423-4_5
Sokolovskii, M.N.: Diagnostic experiments with automata. Cybernetics 7(6), 988–994 (1971). https://doi.org/10.1007/BF01068822
Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78917-8_1
Willemse, T.A.C.: Heuristics for ioco-based test-based modelling. In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds.) FMICS 2006. LNCS, vol. 4346, pp. 132–147. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-70952-7_9
Yannakakis, M., Lee, D.: Testing finite state machines: fault detection. J. Comput. Syst. Sci. 50(2), 209–227 (1995). https://doi.org/10.1006/jcss.1995.1019. http://www.sciencedirect.com/science/article/pii/S0022000085710197
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
van den Bos, P., Vaandrager, F. (2020). State Identification for Labeled Transition Systems with Inputs and Outputs. In: Arbab, F., Jongmans, SS. (eds) Formal Aspects of Component Software. FACS 2019. Lecture Notes in Computer Science(), vol 12018. Springer, Cham. https://doi.org/10.1007/978-3-030-40914-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-40914-2_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-40913-5
Online ISBN: 978-3-030-40914-2
eBook Packages: Computer ScienceComputer Science (R0)