Document Open Access Logo

The Best of Both Worlds: Model-Driven Engineering Meets Model-Based Testing

Authors P. H. M. van Spaendonck , Tim A. C. Willemse

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.4.pdf
  • Filesize: 0.68 MB
  • 16 pages

Document Identifiers

Author Details

P. H. M. van Spaendonck
  • Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands
Tim A. C. Willemse
  • Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands
  • ESI (TNO), Eindhoven, The Netherlands

Funding

  • van Spaendonck, P. H. M.: This publication is part of the PVSR project (project number 17933) of the MasCot research programme which is financed by the Dutch Research Council (NWO).

Acknowledgements

The authors would like to thank Rutger van Beusekom (Verum) for pointing them to the research question that led to this work. Furthermore, the authors would like to thank Jan Tretmans, and the anonymous referees, for feedback on an earlier version of this work.

Cite As Get BibTex

P. H. M. van Spaendonck and Tim A. C. Willemse. The Best of Both Worlds: Model-Driven Engineering Meets Model-Based Testing. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CONCUR.2023.4

Abstract

We study the connection between stable-failures refinement and the ioco conformance relation. Both behavioural relations underlie methodologies that have gained traction in industry: stable-failures refinement is used in several commercial Model-Driven Engineering tool suites, whereas the ioco conformance relation is used in Model-Based Testing tools. Refinement-based Model-Driven Engineering approaches promise to generate executable code from high-level models, thus guaranteeing that the code upholds specified behavioural contracts. Manual testing, however, is still required to gain confidence that the model-to-code transformation and the execution platform do not lead to unexpected contract violations. We identify conditions under which also this last step in the design methodology can be automated using the ioco conformance relation and the associated tools.

Subject Classification

ACM Subject Classification
  • Theory of computation
  • Software and its engineering → Formal software verification
Keywords
  • stable-failures refinement
  • Model-Driven Engineering
  • input output conformance
  • Input Output Labelled Transition Systems
  • internal choice

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. James Baxter, Ana Cavalcanti, Maciej Gazda, and Robert M. Hierons. Testing using CSP models: Time, inputs, and outputs. ACM Trans. Comput. Log., 24(2):17:1-17:40, 2023. URL: https://doi.org/10.1145/3572837.
  2. Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A. C. Willemse. The mCRL2 toolset for analysing concurrent systems - improvements in expressivity and usability. In TACAS (2), volume 11428 of Lecture Notes in Computer Science, pages 21-39. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17465-1_2.
  3. Ana Cavalcanti and Marie-Claude Gaudel. Testing for refinement in CSP. In ICFEM, volume 4789 of Lecture Notes in Computer Science, pages 151-170. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-76650-6_10.
  4. Ana Cavalcanti and Robert M. Hierons. Testing with inputs and outputs in CSP. In FASE, volume 7793 of Lecture Notes in Computer Science, pages 359-374. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37057-1_26.
  5. Ana Cavalcanti, Robert M. Hierons, and Sidney C. Nogueira. Inputs and outputs in CSP: A model and a testing theory. ACM Trans. Comput. Log., 21(3):24:1-24:53, 2020. URL: https://doi.org/10.1145/3379508.
  6. Cocotec. Coco platform. https://cocotec.io/, 2023. Accessed: 01 May 2023.
  7. Marie-Claude Gaudel. Testing can be formal, too. In TAPSOFT, volume 915 of Lecture Notes in Computer Science, pages 82-96. Springer, 1995. URL: https://doi.org/10.1007/3-540-59293-8_188.
  8. Jan Friso Groote, Jeroen J. A. Keiren, Bas Luttik, Erik P. de Vink, and Tim A. C. Willemse. Modelling and analysing software in mCRL2. In FACS, volume 12018 of Lecture Notes in Computer Science, pages 25-48. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-40914-2_2.
  9. Ramon Janssen, Frits W. Vaandrager, and Jan Tretmans. Relating alternating relations for conformance and refinement. In IFM, volume 11918 of Lecture Notes in Computer Science, pages 246-264. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-34968-4_14.
  10. Maurice Laveaux, Jan Friso Groote, and Tim A. C. Willemse. Correct and efficient antichain algorithms for refinement checking. Log. Methods Comput. Sci., 17(1), 2021. URL: https://doi.org/10.23638/LMCS-17(1:8)2021.
  11. Sidney C. Nogueira, Augusto Sampaio, and Alexandre Mota. Test generation from state based use case models. Formal Aspects Comput., 26(3):441-490, 2014. URL: https://doi.org/10.1007/s00165-012-0258-z.
  12. Neda Noroozi, Ramtin Khosravi, Mohammad Reza Mousavi, and Tim A. C. Willemse. Synchronizing asynchronous conformance testing. In SEFM, volume 7041 of Lecture Notes in Computer Science, pages 334-349. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24690-6_23.
  13. Neda Noroozi, Ramtin Khosravi, Mohammad Reza Mousavi, and Tim A. C. Willemse. Synchrony and asynchrony in conformance testing. Softw. Syst. Model., 14(1):149-172, 2015. URL: https://doi.org/10.1007/s10270-012-0302-8.
  14. Jan Peleska, Wen-ling Huang, and Ana Cavalcanti. Finite complete suites for CSP refinement testing. Sci. Comput. Program., 179:1-23, 2019. URL: https://doi.org/10.1016/j.scico.2019.04.004.
  15. A. W. Roscoe. Understanding Concurrent Systems. Texts in Computer Science. Springer, 2010. URL: https://doi.org/10.1007/978-1-84882-258-0.
  16. Julien Schmaltz and Jan Tretmans. On conformance testing for timed systems. In FORMATS, volume 5215 of Lecture Notes in Computer Science, pages 250-264. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85778-5_18.
  17. Jan Tretmans. Testing concurrent systems: A formal approach. In CONCUR, volume 1664 of Lecture Notes in Computer Science, pages 46-65. Springer, 1999. URL: https://doi.org/10.1007/3-540-48320-9_6.
  18. Jan Tretmans. Model based testing with labelled transition systems. In Formal Methods and Testing, volume 4949 of Lecture Notes in Computer Science, pages 1-38. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78917-8_1.
  19. Jan Tretmans and Ramon Janssen. Goodbye ioco. In A Journey from Process Algebra via Timed Automata to Model Learning, volume 13560 of Lecture Notes in Computer Science, pages 491-511. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15629-8_26.
  20. Rutger van Beusekom, Bert de Jonge, Paul F. Hoogendijk, and Jan Nieuwenhuizen. Dezyne: Paving the way to practical formal software engineering. In F-IDE@NFM, volume 338 of EPTCS, pages 19-30, 2021. URL: https://doi.org/10.4204/EPTCS.338.4.
  21. Rutger van Beusekom, Jan Friso Groote, Paul F. Hoogendijk, Robert Howe, Wieger Wesselink, Rob Wieringa, and Tim A. C. Willemse. Formalising the Dezyne modelling language in mCRL2. In FMICS-AVoCS, volume 10471 of Lecture Notes in Computer Science, pages 217-233. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-67113-0_14.
  22. Petra van den Bos and Mariëlle Stoelinga. Tester versus bug: A generic framework for model-based testing via games. In GandALF, volume 277 of EPTCS, pages 118-132, 2018. URL: https://doi.org/10.4204/EPTCS.277.9.
  23. Machiel van der Bijl, Arend Rensink, and Jan Tretmans. Compositional testing with ioco. In FATES, volume 2931 of Lecture Notes in Computer Science, pages 86-100. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24617-6_7.
  24. Martin Weiglhofer. Automated Software Conformance Testing. PhD thesis, Graz University of Technology, 2009. Google Scholar
  25. Martin Weiglhofer and Bernhard K. Aichernig. Unifying input output conformance. In UTP, volume 5713 of Lecture Notes in Computer Science, pages 181-201. Springer, 2008. URL: https://doi.org/10.1007/978-3-642-14521-6_11.
  26. Martin Weiglhofer and Franz Wotawa. Asynchronous input-output conformance testing. In COMPSAC (1), pages 154-159. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/COMPSAC.2009.194.
  27. Tim A. C. Willemse. Heuristics for ioco-based test-based modelling. In FMICS/PDMC, volume 4346 of Lecture Notes in Computer Science, pages 132-147. Springer, 2006. URL: https://doi.org/10.1007/978-3-540-70952-7_9.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact