Advertisement

Relating Alternating Relations for Conformance and Refinement

  • Ramon JanssenEmail author
  • Frits Vaandrager
  • Jan Tretmans
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11918)

Abstract

Various relations have been defined to express refinement and conformance for state-transition systems with inputs and outputs, such as \({\mathbf{ioco}_{\text {}}}\) and \({\mathbf{uioco}}\) in the area of model-based testing, and alternating simulation and alternating-trace containment originating from game theory and formal verification. Several papers have compared these independently developed relations, but these comparisons make assumptions (e.g., input-enabledness), pose restrictions (e.g., determinism – then they all coincide), use different models (e.g., interface automata and Kripke structures), or do not deal with the concept of quiescence. In this paper, we present the integration of the \({\mathbf{ioco}_{\text {}}}\)/\({\mathbf{uioco}}\) theory of model-based testing and the theory of alternating refinements, within the domain of non-deterministic, non-input-enabled interface automata. A standing conjecture is that \({\mathbf{ioco}_{\text {}}}\) and alternating-trace containment coincide. Our main result is that this conjecture does not hold, but that \({\mathbf{uioco}}\) coincides with a variant of alternating-trace containment, for image finite interface automata and with explicit treatment of quiescence. From the comparison between \({\mathbf{ioco}_{\text {}}}\) theory and alternating refinements, we conclude that \({\mathbf{ioco}_{\text {}}}\) and the original relation of alternating-trace containment are too strong for realistic black-box scenarios. We present a refinement relation which can express both \({\mathbf{uioco}}\) and refinement in game theory, while being simpler and having a clearer observational interpretation.

Keywords

Alternating refinement ioco uioco Interface automata 

References

  1. 1.
    Aarts, F., Vaandrager, F.: Learning I/O automata. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 71–85. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15375-4_6CrossRefGoogle Scholar
  2. 2.
    de Alfaro, L., Henzinger, T.A.: Interface automata. In: Gruhn, V. (ed.) Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering, volume 26 of SIGSOFT Software Engineering Notes, pp. 109–120. ACM Press (2001)Google Scholar
  3. 3.
    Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0055622CrossRefGoogle Scholar
  4. 4.
    van der Bijl, M., Rensink, A., Tretmans, J.: Compositional testing with ioco. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 86–100. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24617-6_7CrossRefzbMATHGoogle Scholar
  5. 5.
    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 of the 9th International Symposium on GandALF, Saarbrücken, Germany, Volume 277 of Electronic Proceedings in Theoretical Computer Science, pp. 118–132. Open Publishing Association (2018)Google Scholar
  6. 6.
    Chilton, C., Jonsson, B., Kwiatkowska, M.: An algebraic theory of interface automata. Theor. Comput. Sci. 549, 146–174 (2014)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Frantzen, L., Tretmans, J.: Model-based testing of environmental conformance of components. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 1–25. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-74792-5_1CrossRefzbMATHGoogle Scholar
  8. 8.
    van Glabbeek, R.J.: The linear time – branching time spectrum I. The semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 3–99. North-Holland (2001)Google Scholar
  9. 9.
    Heerink, L., Tretmans, J.: Refusal testing for classes of transition systems with inputs and outputs. In: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A. (eds.) Formal Description Techniques and Protocol Specification, Testing and Verification FORTE X /PSTV XVII, pp. 23–38. Chapman & Hall (1997)Google Scholar
  10. 10.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Boston (1979)zbMATHGoogle Scholar
  11. 11.
    Janssen, R., Tretmans, J.: Matching implementations to specifications: the corner cases of IOCO. In: Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, Limassol, Cyprus, pp. 2196–2205. ACM (2019)Google Scholar
  12. 12.
    Janssen, R., Vaandrager, F., Tretmans, J.: Relating alternating relations for conformance and refinement (2019). https://arxiv.org/pdf/1909.13604.pdf
  13. 13.
    Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. MIT Laboratory for Computer Science (1988)Google Scholar
  14. 14.
    Mostowski, W., Poll, E., Schmaltz, J., Tretmans, J., Wichers Schreur, R.: Model-based testing of electronic passports. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 207–209. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-04570-7_19CrossRefGoogle Scholar
  15. 15.
    Reingold, N., Wang, D.-W., Zuck, L.D.: Games I/O automata play. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 325–339. Springer, Heidelberg (1992).  https://doi.org/10.1007/BFb0084801CrossRefGoogle Scholar
  16. 16.
    Segala, R., Gawlick, R., Søgaard-Andersen, J.F., Lynch, N.A.: Liveness in timed and untimed systems. Inf. Comput. 141(2), 119–171 (1998)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Softw.-Concepts Tools 17(3), 103–120 (1996)zbMATHGoogle Scholar
  18. 18.
    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_1CrossRefGoogle Scholar
  19. 19.
    Tretmans, J.: On the existence of practical testers. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 87–106. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-68270-9_5CrossRefGoogle Scholar
  20. 20.
    Veanes, M., Bjørner, N.: Alternating simulation and IOCO. Int. J. Softw. Tools Technol. Transf. 14(4), 387–405 (2012)CrossRefGoogle Scholar
  21. 21.
    Volpato, M., Tretmans, J.: Towards quality of model-based testing in the IOCO framework. In: International Workshop on Joining AcadeMiA and Industry Contributions to testing Automation - JAMAICA 2013, pp. 41–46. ACM (2013)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Ramon Janssen
    • 1
    Email author
  • Frits Vaandrager
    • 1
  • Jan Tretmans
    • 1
    • 2
  1. 1.Radboud UniversityNijmegenThe Netherlands
  2. 2.ESI (TNO)EindhovenThe Netherlands

Personalised recommendations