Editorial for the special issue of STVR on tests and proofs volume 1: tests and proofs in model-based testing

The increasing use of IT systems in security or safety critical areas as well as growing system complexity creates challenges for both formal verification and testing. It might initially appear that these are competing techniques: it can be argued that once a program is proven to be correct, there is no need for additional tests. Similarly, if it is not feasible to produce a formal proof, then one cannot do better than testing your program thoroughly. As a consequence of this perception, proofs and tests have been pursued by distinct communities using rather different techniques and tools. Despite this historical separation of work on testing and proof, research in these areas has led to the discovery of common issues and to the realisation that each may need the other. The emergence of model checking was one of the first signs that contradictions contribute to testing, but in the past few years an increasing number of researchers have encountered the need to combine proofs and tests, dropping earlier dogmatic views of incompatibility and taking instead the best of what each of these software engineering domains has to offer. This special issue of STVR tries to bring together researchers and practitioners working in the converging fields of testing and proving. We received 16 submissions for this special issue. Reviewing followed the same process as for regular papers. Each paper was reviewed by at least three reviewers, and after a rigorous selection process requiring a total of 33 revisions and 75 reviews, seven papers remain for publication. These papers are spread across two special issues of STVR and discuss two different aspects of tests and proofs: model-based testing and approaches for improving the quality of generated test data. This first volume includes the first three papers, covering the use of tests and proof in model-based testing. The first paper, “Test generation with SMT solvers in Model-Based Testing” by Jérôme Cantenot, Fabrice Ambert, and Fabrice Bouquet presents a framework for generating test cases from a subset of UML (class models, object models, and state modes) that are enriched with constraints expressed in OCL. The developed test generation methods ensure that each operation and transition of the model is stimulated at least once during test execution. The second paper, “Test Generation from Recursive Tile Systems” by Sébastien Chédor, Thierry Jéron, and Christophe Morvan explores the generation of conformance test cases from recursive tile systems models. The authors discuss both on-line and off-line test cases for recursive tile systems within the ioco framework. The third paper, “Model Based Testing for Concurrent Systems with Labeled Event Structures” by Hernán Ponce de León, Stefan Haar, and Delphine Longuet presents a model-based approach for testing concurrent systems. The concurrent systems are modeled using labeled event structures and their test case generation algorithm is able to derive a sound and exhaustive test suite from these models. All the contributions presented in this and the upcoming special issue on Tests and Proofs reveal the broad and dynamic community that works on the intersection of tests and proofs. This was only possible through the combined efforts of all authors and reviewers, and we wish to thank them all for their time and energy. The following persons were reviewers: Paul Ammann, Lukas Brügger, Fabian Büttner, Cristian Cadar, George Candea, John Derrick, Catherine Dubois, Alessandro Fantechi, Vijay Ganesh, Angelo Gargantini, Ryszard Janicki, Thierry Jéron, Tomoji Kishi, Nils Klarlund, Nikolai Kosmatov, Moez Krichen, Pascale Le Gall, Bruno Legeard, Zdenek Letko, Xuandong Li, Karl Meinke, Magnus Myreen, Joseph Near, Virginia Papailiopoulou, Jan Peleska, Dennis Peters, Alexander Pretschner, Antoine Rollet, Kristin Y. Rozier, Andy Schurr, Thomas Sewell, Tomohiko Takagi, Andreas Teucke, T.H. Tse, Mark Utting, Machiel van der Bijl, Luca Viganò, Birgit Vogel-Heuser, Tjark Weber, Stephan Weissleder, Tim A.C. Willemse,