Published: 10th April 2015
DOI: 10.4204/EPTCS.180
ISSN: 2075-2180


Proceedings Tenth Workshop on
Model Based Testing
London, UK, 18th April 2015

Edited by: Nikolay Pakulin, Alexander K. Petrenko and Bernd-Holger Schlingloff

Using Model Checking to Generate Test Cases for Android Applications
Ana Rosario Espada, María del Mar Gallardo, Alberto Salmerón and Pedro Merino
ioco theory for probabilistic automata
Marcus Gerhold and Mariëlle Stoelinga
A Visual Formalism for Interacting Systems
Paul C. Jorgensen
Potential Errors and Test Assessment in Software Product Line Engineering
Hartmut Lackner and Martin Schmidt
Adaptive Homing is in P
Natalia Kushik and Nina Yevtushenko


This volume contains the proceedings of the 10th Workshop on Model-Based Testing (MBT 2015), held in London on April 18th, 2015, as a satellite workshop of the European Joint Conferences on Theory and Practice of Software (ETAPS 2015). The first Workshop on Model-Based Testing in this series took place in 2004, in Barcelona.

A tenth anniversary is a good opportunity to look back and to strike a balance, analyzing tendencies of investigations in MBT for the last 10+ years. This preface is not aimed at a thorough analysis; a flavor of the topics under consideration can be tasted by reviewing the invited papers made at the previous MBT workshops. We would like to give a short retrospective on MBT beginning with a talk of Alan Harman, made in 2006, because of its notable title: Ten Years of Model Based Testing - A sober evaluation [6]. The title of the talk claims that model-based testing has started at about 1996. In fact, MBT appeared already in the 1970s, and, apparently, even earlier. The main MBT applications in those years were in the field of testing hardware logic and telecommunication protocols. The main modeling paradigms in this field were Finite-State machine, Petri nets and other transition systems. The late 1990s is the period when the community understood that this approach can be effectively used not only for a rather narrow class of tasks close to telecommunication protocols, but also for practically all types of software, including operating systems, compilers, DBMS and others. This new approach to MBT immediately set the task to seek more adequate modeling paradigms for a new class of target systems. As the result the developers began to investigate requirement specification in the form of assertions or constraints and their special cases for program contracts.

Apparently, this new trend of MBT applications was reflected in articles such as T. J. Ostrand and M. J. Balcer's The Category-Partition Method for Specifying and Generating Functional Tests [7]. This method later became known as CPM. The essence of the CPM method is to design tests on the basis of a certain state machine, the states of which correspond to the domains of input space, i.e., partitions.

Those input space domains, in turn, correspond to the data domains where predicates making up the assertions of functional specification of the system under test operations take true or false values - that is, the input space is divided into partitions according to the terms described in specifications of functional requirements to operations under test.

Ostrand and Balcer offered a certain method of projecting tests. However, nothing was said about the tools supporting those methods. Probably, one of the first works aimed at designing a tool kit to support the method was the KVEST technology (I. Burdonov, A. Kossatchev, A.K.Petrenko, D. Galter KVEST: Automated Generation of Test Suites from Formal Specifications [3]) and the following UniTESK technology (I. Bourdonov, A. Kossatchev, V. Kuliamin, and A.K. Petrenko. UniTesK Test Suite Architecture [2]). Both technologies were based on the experience of the development testing methodology within the frames of Space Shuttle «Buran» designed in the late 1980s (A.K.Petrenko. Test specification based on trace description [8]).

This stage of MBT development was advanced with the emergence of test generation based on abstract state machines (W. Grieskamp, Y. Gurevich, W. Schulte, and M. Veanes. Conformance Testing with Abstract State Machines [4]), followed by SpecExplorer (A. Blass, Y. Gurevich, L. Nachmanson, and M. Veanes. Play to test [1]) in 2005.

At the end of 2002, the idea appeared to organize MBT workshop as a satellite event of ETAPS-2004, and devote it to testing on the basis of formal models - the idea that was gaining more and more supporters that time. We decided not to restrict it to only a certain narrow class of models or test generation techniques. Thus, from the very first workshops there were supporters of many different variations of MBT.

Invited talks of the MBT workshops show, on the one hand, that rather a wide range of work has been carried out in the field of MBT and, on the other hand, suggest some reflections. In particular, it is interesting to note that in the beginning of the list, practitioners prevailed, while towards the end of the list theoreticians dominate. Why so? We could imagine a couple of potential reasons:

  1. Firstly, when this new theme was developing, practitioners were invited to show convincing use cases of MBT in large-scale industrial projects.
  2. Secondly, it seems that in recent years practical MBT tools reached their limit in utilizing existing techniques: by now the tools have implemented most of what can be achieved at the present technological level. However, the development does not end here; we face a period of accumulating new knowledge that will make new fundamental advances in practical MBT development possible. Therefore, in recent years interest has shifted towards more theoretical research questions.

And one more observation: we can see an obvious predominance of giants such as Microsoft, IBM, Nokia among practitioners (Conformiq is mainly oriented towards Nokia's demands). This can probably be explained by the fact that development of an industrial-strength MBT tool and MBT applications requires significant resources, which are hardly available for small and medium-sized companies.

Observing the list of speakers at recent MBT workshops we can state that there is no prevailing trend in the modeling paradigms or testing techniques employed. On the basis of this observation we propose that different approaches to MBT are, on the one hand, complementary, and, on the other hand, the approaches need both methodological integration and unification on the level of testing system components and unified interfaces. This allows us to implement shared use of model analyzers and program source codes, data generators, provers, systems for collecting and run-time monitoring, etc.

Let us briefly reflect on the perspectives of MBT:

This year's MBT workshop features Ana Cavalli from Institut National des Telecommunications, Paris, France as invited speaker. In her speech, entitled «Evolution of testing techniques: from active testing to monitoring techniques», she presents the evolution of these testing techniques, their advantages and limitations, and illustrates the application of monitoring techniques to the security testing of real case studies.

The contributions selected by the Program Committee reflect both applications of MBT in industrial practice and further development of MBT theory and techniques.

Ana Rosario Espada, Maria Del Mar Gallardo, Alberto Salmerón and Pedro Merino present an approach to automated model construction and test generation for Android mobile applications. Marcus Gerhold and Mariëlle Stoelinga extend the well-known notion of input-output conformance to probabilistic state machines, opening the door to development of new classes of models and test construction techniques. Paul Jorgensen presents a novel variation of Petri-nets to facilitate visual modeling of interacting components in complex systems. Hartmut Lackner and Martin Schmidt discuss quality of test suites for product lines and develop an assessment approach based on mutation operators applied to software product lines. Natalia Kushik and Nina Yevtushenko present new result in the theory of FSM; they show that for some FSMs its homing sequence can be built in polynomial time.

The workshop is concluded by a remotely presented talk by Yury Gurevich on «Testing Philosophy».

We would like to thank the program committee members and all reviewers for their work in evaluating the submissions for the whole period of MBT workshops. We also thank the ETAPS organizers for their assistance in preparing the workshops and the editors of EPTCS for help in publishing these workshop proceedings.

Alexander K. Petrenko,
Holger Schlingloff,
Nikolay Pakulin
March 2015


  1. Andreas Blass, Yuri Gurevich, Lev Nachmanson, and Margus Veanes(2005): Play to test.
    Technical Report MSR-TR-2005-04, Microsoft Research.
    Available at
    A short version appears in: FATES 2005, LNCS vol. 3997, pp. 32-46.

  2. Igor B. Bourdonov, Alexander Kossatchev, Victor V. Kuliamin, and Alexander K. Petrenko (2002): UniTesK Test Suite Architecture.
    In: FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings, pp. 77-88, doi:10.1007/3-540-45614-7_5.

  3. Igor B. Burdonov, Alexander Kossatchev, Alexandre K. Petrenko, and Dmitri Galter (1999): KVEST: Automated Generation of Test Suites from Formal Specifications.
    In: FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume I, pp. 608-621, doi:10.1007/3-540-48119-2_34.

  4. Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte& Margus Veanes (2001): Conformance Testing with Abstract State Machines.
    In R. Moreno-Diaz& A. Quesada-Arencibia, editors: Formal Methods and Tools for Computer Science; Proceedings of Eurocast 2001.
    Available at

  5. Wolfgang Grieskamp, Xiao Qu, Xiangjun Wei, Nicolas Kicillof, and Myra B. Cohen(2009): Interaction Coverage Meets Path Coverage by SMT Constraint Solving.
    In: Testing of Software and Communication Systems, 21st IFIP WG 6.1 International Conference, TESTCOM 2009 and 9th International Workshop, FATES 2009, Eindhoven, The Netherlands, November 2-4, 2009. Proceedings, pp. 97-112, doi:10.1007/978-3-642-05031-2_7.

  6. Alan Hartman(2006): Ten Years of Model Based Testing - A sober evaluation.
    Available at
    Invited talk at the Second Workshop on Model Based Testing March 25-26, 2006 Vienna , Austria.

  7. Thomas J. Ostrand, and Marc J. Balcer (1988): The Category-Partition Method for Specifying and Generating Functional Tests.
    Commun. ACM 31(6), pp. 676-686, doi:10.1145/62959.62964.

  8. Alexander K. Petrenko (1993): Test Specfication Based on Trace Description.
    Programming and Computer Software 19(1).

Program committee