Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Aspects of Component Software

FACS 2019: Formal Aspects of Component Software pp 191–212Cite as

State Identification for Labeled Transition Systems with Inputs and Outputs

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12018))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    This is a variation of Lemma 22 from [5], which is stated for a slightly different composition operator that involves demonic completions. Adding demonic completions is useful in the setting of [5], but not needed for our purposes.

References

  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 

  2. Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)

    MATH  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

  5. 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

    Article  Google Scholar 

  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

  7. Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)

    MATH  Google Scholar 

  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_14

    Chapter  Google Scholar 

  9. 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)

    Article  Google Scholar 

  10. Gill, A.: Introduction to the Theory of Finite-State Machines. McGraw-Hill, New York (1962)

    MATH  Google Scholar 

  11. 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

    Article  Google Scholar 

  12. 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

    Article  MathSciNet  MATH  Google Scholar 

  13. Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines – a survey. Proc. IEEE 84(8), 1090–1123 (1996)

    Article  Google Scholar 

  14. 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

    Chapter  MATH  Google Scholar 

  15. Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)

    MATH  Google Scholar 

  16. Moerman, J.: Nominal techniques and black box testing for automata learning. Ph.D. thesis, Radboud University Nijmegen, July 2019

    Google 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 

  18. 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

    Chapter  Google Scholar 

  19. 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

    Chapter  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 

  23. 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

    Chapter  Google Scholar 

  24. Sokolovskii, M.N.: Diagnostic experiments with automata. Cybernetics 7(6), 988–994 (1971). https://doi.org/10.1007/BF01068822

    Article  MathSciNet  Google Scholar 

  25. 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

    Chapter  Google Scholar 

  26. 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

    Chapter  Google Scholar 

  27. 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

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands

    Petra van den Bos & Frits Vaandrager

Authors
  1. Petra van den Bos
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frits Vaandrager
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Petra van den Bos .

Editor information

Editors and Affiliations

  1. CWI, University of Leiden, Leiden, The Netherlands

    Farhad Arbab

  2. Open University of the Netherlands, Heerlen, The Netherlands

    Sung-Shik Jongmans

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation