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.
Funded by the Netherlands Organisation of Scientific Research (NWO-TTW), project 13859: SUMBAT - SUpersizing Model-BAsed Testing.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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_6
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)
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/BFb0055622
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_7
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)
Chilton, C., Jonsson, B., Kwiatkowska, M.: An algebraic theory of interface automata. Theor. Comput. Sci. 549, 146–174 (2014)
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_1
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)
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)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Boston (1979)
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)
Janssen, R., Vaandrager, F., Tretmans, J.: Relating alternating relations for conformance and refinement (2019). https://arxiv.org/pdf/1909.13604.pdf
Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. MIT Laboratory for Computer Science (1988)
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_19
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/BFb0084801
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)
Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Softw.-Concepts Tools 17(3), 103–120 (1996)
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
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_5
Veanes, M., Bjørner, N.: Alternating simulation and IOCO. Int. J. Softw. Tools Technol. Transf. 14(4), 387–405 (2012)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Janssen, R., Vaandrager, F., Tretmans, J. (2019). Relating Alternating Relations for Conformance and Refinement. In: Ahrendt, W., Tapia Tarifa, S. (eds) Integrated Formal Methods. IFM 2019. Lecture Notes in Computer Science(), vol 11918. Springer, Cham. https://doi.org/10.1007/978-3-030-34968-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-34968-4_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-34967-7
Online ISBN: 978-3-030-34968-4
eBook Packages: Computer ScienceComputer Science (R0)