Ramon Janssen
ABSTRACT
A well-known conformance relation for model-based testing is ioco. A conformance relation expresses when an implementation is correct with respect to a specification. Unlike many other conformance and refinement relations, ioco has different domains for implementations and for specifications. Consequently, ioco is neither reflexive nor transitive, implying that a specification does not implement itself, and that specifications cannot be compared for refinement. In this paper, we investigate how we can compensate for the lack of reflexivity and transitivity. We show that (i) given a specification, we can construct in a standard way a canonical conforming implementation that is very 'close' to the specification; and (ii) a refinement preorder on specification models can be defined such that a refined model allows less ioco-conforming implementations. We give declarative and constructive definitions of both, we give examples of unimplementable corner-cases, we investigate decidability, and we do that for ioco as well as for the ioco-variant uioco. The latter turns out to be simpler and on more aspects decidable.
- L. de Alfaro and T.A. Henzinger. Interface Automata. In V. Gruhn, editor, ESEC/FSE'01, SIGSOFT Softw. Eng. Notes 26, pages 109--120. ACM Press, 2001. Google Scholar
Digital Library
- N. Beneš, P. Daca, T.A. Henzinger, J. Křetínskỳ, and D. Ničković. Complete composition operators for ioco-testing theory. In P. Kruchten et al., editors, ACM SIGSOFT Symp. on Comp.-Based Softw. Eng., pages 101--110. ACM, 2015. Google ScholarDigital Library
- JA Bergstra, JCM Baeten, and Jan Willem Klop. On the consistency of Koomen's fair abstraction rule. TCS, 37(1):129--176, 1987. Google ScholarDigital Library
- M. van der Bijl, A. Rensink, and J. Tretmans. Compositional Testing with ioco. In A. Petrenko and A. Ulrich, editors, FATES 2003, LNCS 2931, pages 86--100. Springer-Verlag, 2004.Google Scholar
- I.B. Bourdonov and A.S. Kossatchev. Specification completion for IOCO. Programming and Computer Softw., 37(1):1--14, 2011. Google ScholarDigital Library
- L. Frantzen, J. Tretmans, and T.A.C. Willemse. A Symbolic Framework for Model-Based Testing. In K. Havelund et al., editors, FATES/RV'06, LNCS 4262, pages 40--54. Springer-Verlag, 2006. Google ScholarDigital Library
- M.-C. Gaudel. Testing can be Formal, too. In P.D. Mosses et al., editors, TAP-SOFT'95, LNCS 915, pages 82--96. Springer-Verlag, 1995. Google ScholarDigital Library
- Marcus Gerhold and Mariëlle Stoelinga. Model-based testing of probabilistic systems. Formal Aspects of Computing, 30(1):77--106, 2018. Google ScholarDigital Library
- C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. Google ScholarDigital Library
- R. Janssen and J. Tretmans. Matching implementations to specifications: The corner cases of ioco. Technical report, 2019. URL https://sumbat.cs.ru.nl/Publications?action=upload&upname=JanssenTretmansCornerCasesOfIoco.pdf.Google ScholarDigital Library
- M. Krichen and S. Tripakis. Black-Box Conformance Testing for Real-Time Systems. In S. Graf and others., editors, SPIN'04, LNCS 2989. Springer-Verlag, 2004.Google ScholarCross Ref
- Malte Lochau, Sven Peldszus, Matthias Kowal, and Ina Schaefer. Model-based testing. In M. Bernardo et al., editors, Formal Methods for the Design of Computer, Communication and Softw. Systems, 2014.Google Scholar
- Anil Nerode. Linear automaton transformations. Proc. of the American Mathematical Society, 9(4):541--544, 1958.Google ScholarCross Ref
- N. Noroozi. Improving Input-Output Conformance Testing Theories. PhD thesis, Eindhoven University of Technology, Eindhoven (NL), 2014.Google Scholar
- Larry J Stockmeyer and Albert R Meyer. Word problems requiring exponential time. In Proc. 5th ACM Symp. on Theory of computing, pages 1--9. ACM, 1973. Google ScholarDigital Library
- G. Stokkink, M. Timmer, and M. Stoelinga. Talking quiescence: a rigorous theory that supports parallel composition, action hiding and determinisation. In A. K. Petrenko and H. Schlingloff, editors, MBT'12, volume 80 of EPTCS, 2012.Google Scholar
- J. Tretmans. Test Generation with Inputs, Outputs and Repetitive Quiescence. Software---Concepts and Tools, 17(3):103--120, 1996.Google Scholar
- J. Tretmans. Model Based Testing with Labelled Transition Systems. In R.M. Hierons et al., editors, Formal Methods and Testing, LNCS 4949, pages 1--38. Springer-Verlag, 2008. Google ScholarDigital Library
- M. Volpato and J. Tretmans. Towards Quality of Model-Based Testing in the ioco Framework. In JAMAICA'13, pages 41--46, New York, NY, USA, 2013. ACM. Google ScholarDigital Library
- T.A.C. Willemse. Heuristics for ioco-Based Test-Based Modelling. In L. Brim et al., editors, FMICS/PDMC'07, LNCS 4346, pages 123--147. Springer-Verlag, 2007. Google ScholarDigital Library
Recommendations
Protective Interface Specifications
Abstract.The interface specification of a procedure describes the procedure's behaviour using pre- and postconditions. These pre- and postconditions are written using various functions. If some of these functions are partial, or underspecified, then the ...
Compiling Modechart specifications
RTSS '95: Proceedings of the 16th IEEE Real-Time Systems SymposiumThe Modechart specification language is a formalism for the specification of real-time systems. A toolset for specification, analysis and simulation for Modechart specifications exists for supporting the design and construction of real-time systems. ...
Comments