Monadic Sequence Testing and Explicit Test-Refinements

  • Achim D. BruckerEmail author
  • Burkhart Wolff
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9762)


We present an abstract framework for sequence testing that is implemented in Isabelle/HOL-TestGen. Our framework is based on the theory of state-exception monads, explicitly modelled in HOL, and can cope with typed input and output, interleaving executions including abort, and synchronisation.

The framework is particularly geared towards symbolic execution and has proven effective in several large case-studies involving system models based on large (or infinite) state.

On this basis, we rephrase the concept of test-refinements for inclusion, deadlock and IOCO-like tests, together with a formal theory of its relation to traditional, IO-automata based notions.


Monadic sequence testing framework HOL-TestGen 



This work was partially supported by the Euro-MILS project funded by the European Union’s Programme [FP7/2007-2013] under grant agreement number ICT-318353.


  1. 1.
    Andrews, P.B.: Introduction to Mathematical Logic and Type Theory: To Truth through Proof, 2nd edn. Kluwer Academic Publishers, Dordrecht (2002)CrossRefzbMATHGoogle Scholar
  2. 2.
    Brucker, A.D., Brügger, L., Wolff, B.: Formal firewall conformance testing: An application of test and proof techniques. Softw. Testing Verif. Reliab. (STVR) 25(1), 34–71 (2015)CrossRefGoogle Scholar
  3. 3.
    Brucker, A.D., Feliachi, A., Nemouchi, Y., Wolff, B.: Test program generation for a microprocessor. In: Veanes, M., Viganò, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 76–95. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  4. 4.
    Brucker, A.D., Havle, O., Nemouchi, Y., Wolff, B.: Testing the IPC protocol for a real-time operating system. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 40–60. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-29613-5_3 CrossRefGoogle Scholar
  5. 5.
    Brucker, A.D., Wolff, B.: Test-sequence generation with Hol-TestGen with an application to firewall testing. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 149–168. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  6. 6.
    Brucker, A.D., Wolff, B.: On theorem prover-based testing. Formal Aspects Comput. (FAC) 25(5), 683–721 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Cheng, K.T., Krishnakumar, A.S.: Automatic functional test generation using the extended finite state machine model. In: International Design Automation Conference, DAC 1993, pp. 86–91. ACM, New York (1993)Google Scholar
  8. 8.
    Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5(2), 56–68 (1940)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    D’Antoni, L., Veanes, M.: Minimization of symbolic automata. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 541–554. ACM (2014)Google Scholar
  10. 10.
    Feliachi, A., Gaudel, M., Wenzel, M., Wolff, B.: The circus testing theory revisited in Isabelle/HOL. In: Formal Methods and Software Engineering, pp. 131–147 (2013)Google Scholar
  11. 11.
    Fraenkel, A., Bar-Hillel, Y.: Foundations of Set Theory. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1958)zbMATHGoogle Scholar
  12. 12.
    Frantzen, L., Tretmans, J., Willemse, T.A.C.: A symbolic framework for model-based testing. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds.) FATES 2006 and RV 2006. LNCS, vol. 4262, pp. 40–54. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Gill, A.: Introduction to the Theory of Finite-State Machines. McGraw-Hill, New York (1962)zbMATHGoogle Scholar
  14. 14.
    Halmos, P.: Naive Set Theory. Undergraduate Texts in Mathematics. Springer, New York (1974)CrossRefzbMATHGoogle Scholar
  15. 15.
    Jard, C., Jéron, T.: TGV: theory, principles and algorithms. STTT 7(4), 297–315 (2005)CrossRefGoogle Scholar
  16. 16.
    Jéron, T.: Symbolic model-based test selection. Electr. Notes Theor. Comput. Sci. 240, 167–184 (2009)CrossRefzbMATHGoogle Scholar
  17. 17.
    Kalaji, A.S., Hierons, R.M., Swift, S.: Generating feasible transition paths for testing from an extended finite state machine (EFSM) with the counter problem. In: Third International Conference on Software Testing, Verification and Validation, ICST, pp. 232–235. IEEE Computer Society (2010)Google Scholar
  18. 18.
    Ponce de León, H., Haar, S., Longuet, D.: Conformance relations for labeled event structures. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol. 7305, pp. 83–98. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  19. 19.
    Lynch, N., Tuttle, M.: An introduction to input/output automata. CWI-Quarterly 2(3), 219–246 (1989)MathSciNetzbMATHGoogle Scholar
  20. 20.
    Mealy, G.H.: A method for synthesizing sequential circuits. Bell Syst. Tech. J. 34(5), 1045–1079 (1955)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Moore, E.F.: Gedanken-experiments on sequential machines. In: Shannon, C., McCarthy, J. (eds.) Automata Studies, pp. 129–153. Princeton University Press, Princeton (1956)Google Scholar
  22. 22.
    Rusu, V., Marchand, H., Jéron, T.: Automatic verification and conformance testing for validating safety properties of reactive systems. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 189–204. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  23. 23.
    Tretmanns, J., Belifante, Z.: Automatic testign with formal methods. In: 7th European International Conference on Software Testing, Analysis and Review (EuroSTAR 1999) (1999)Google Scholar
  24. 24.
    Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Soft. Concepts Tools 17(3), 103–120 (1996)zbMATHGoogle Scholar
  25. 25.
    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)CrossRefGoogle Scholar
  26. 26.
    Veanes, M., Bjørner, N.: Alternating simulation and IOCO. STTT 14(4), 387–405 (2012)CrossRefGoogle Scholar
  27. 27.
    Veanes, M., Bjørner, N.: Symbolic automata: the toolkit. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 472–477. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  28. 28.
    Wadler, P.: Comprehending monads. Math. Struct. Comput. Sci. 2(4), 461–493 (1992)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Department of Computer ScienceThe University of SheffieldSheffieldUK
  2. 2.LRI, Univ Paris Sud, CNRS, Centrale Suplélec, Université SaclayOrsayFrance

Personalised recommendations