Abstract
In this paper we continue the study of the input-output conformance simulation (ioco s). In particular, we focus on implementation aspects to show that ioco s is indeed an interesting semantic relation for formal methods. We address two complementary issues: a) In the context of model based testing (MBT) we present an online, also called on-the-fly, testing algorithm that checks whether an implementation conforms a given specification. Online testing combines test generation and execution and avoids the generation of the complete test suite for the specification. We prove both soundness and completeness of the online algorithm with respect to the ioco s relation. b) In the context of formal verification and model checking minimisation a key issue is to efficiently compute the considered semantic relations; we show how the coinductive flavour of our conformance relation ioco s makes it appropriate to be cast into an instance of the Generalised Coarsest Partition Problem (GCPP) and thus it can be efficiently computed.
Research partially supported by the Spanish MEC projects TIN2009-14312-C02-01 and TIN2012-36812-C02-01.
Chapter PDF
Similar content being viewed by others
Keywords
References
Abramsky, S.: Observational equivalence as a testing equivalence. Theoretical Computer Science 53(3), 225–241 (1987)
Aceto, L., de Frutos Escrig, D., Gregorio-Rodrguez, C., Ingolfsdottir, A.: Axiomatizing weak simulation semantics over BCCSP. Theoretical Computer Science (March 26, 2013) (to appear)
Belinfante, A.: Jtorx: A tool for on-line model-driven test derivation and execution. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 266–270. Springer, Heidelberg (2010)
Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. Journal of the ACM 42(1), 232–268 (1995)
Bulychev, P., Chatain, T., David, A., Larsen, K.G.: Efficient on-the-fly algorithm for checking alternating timed simulation. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 73–87. Springer, Heidelberg (2009)
Bustan, D., Grumberg, O.: Simulation-based minimization. ACM Trans. Comput. Logic 4(2), 181–206 (2003)
Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, W., Willemse, T.A.C.: An overview of the mcrl2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 199–213. Springer, Heidelberg (2013)
de Frutos-Escrig, D., Gregorio-Rodríguez, C., Palomino, M., Romero-Hernández, D.: Unifying the linear time-branching time spectrum of process semantics. Logical Methods in Computer Science 9(2:11), 1–74 (2013)
de Vries, R.G., Tretmans, J.: On-the-fly conformance testing using spin. STTT 2(4), 382–393 (2000)
Fábregas, I., de Frutos Escrig, D., Palomino, M.: Logics for contravariant simulations. In: Hatcliff, J., Zucca, E. (eds.) FMOODS 2010, Part II. LNCS, vol. 6117, pp. 224–231. Springer, Heidelberg (2010)
Gentilini, R., Piazza, C., Policriti, A.: From bisimulation to simulation: Coarsest partition problems. J. Autom. Reasoning 31(1), 73–103 (2003)
Gregorio-Rodríguez, C., Llana, L., Martínez-Torres, R.: Input-output conformance simulation (iocos) for model based testing. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE 2013. LNCS, vol. 7892, pp. 114–129. Springer, Heidelberg (2013)
Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Information and Computation 86(1), 43–68 (1990)
Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007)
Larsen, K.G., Mikucionis, M., Nielsen, B.: Online testing of real-time systems using UPPAAL. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 79–94. Springer, Heidelberg (2005)
Llana, L., Martínez-Torres, R.: Ioco as a simulation. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 125–134. Springer, Heidelberg (2014)
Lüttgen, G., Vogler, W.: Ready simulation for concurrency: It’s logical? Information and Computation 208(7), 845–867 (2010)
Milner, R.: An algebraic definition of simulation between programs. In: Proceedings 2nd Joint Conference on Artificial Intelligence, pp. 481–489. BCS (1971), Report No. CS-205, Computer Science Department, Stanford University
Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Milner, R.: Communication and Concurrency. Prentice Hall (1989)
Rabanal, P., Rodríguez, I., Rubio, F.: Testing restorable systems: formal definition and heuristic solution based on river formation dynamics. Formal Aspects of Computing 25(5), 743–768 (2013)
Ranzato, F.: A More Efficient Simulation Algorithm on Kripke Structures. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 753–764. Springer, Heidelberg (2013)
Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Preliminary report. In: Aho, A.V., Borodin, A., Constable, R.L., Floyd, R.W., Harrison, M.A., Karp, R.M., Strong, H.R. (eds.) STOC, pp. 1–9. ACM (1973)
Stokkink, G., Timmer, M., Stoelinga, M.: Talking quiescence: a rigorous theory that supports parallel composition, action hiding and determinisation. In: Petrenko, A.K., Schlingloff, H. (eds.) MBT. EPTCS, vol. 80, pp. 73–87 (2012)
Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008)
Tretmans, J., Brinksma, E.: Torx: Automated model-based testing. In: Hartman, A., Dussa-Ziegler, K. (eds.) First European Conference on Model-Driven Software Engineering, pp. 31–43 (December 2003)
van Glabbeek, R.J.: The Linear Time – Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes. In: Handbook of Process Algebra, pp. 3–99. Elsevier (2001)
van Glabbeek, R.J., Ploeger, B.: Correcting a space-efficient simulation algorithm. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 517–529. Springer, Heidelberg (2008)
Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: Wermelinger, M., Gall, H. (eds.) ESEC/SIGSOFT FSE, pp. 273–282. ACM (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Gregorio-Rodríguez, C., Llana, L., Martínez-Torres, R. (2014). Effectiveness for Input Output Conformance Simulation iocos̱. In: Ábrahám, E., Palamidessi, C. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2014. Lecture Notes in Computer Science, vol 8461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-43613-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-662-43613-4_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-43612-7
Online ISBN: 978-3-662-43613-4
eBook Packages: Computer ScienceComputer Science (R0)