Catálogo de publicaciones - libros

For half a decade model-based testing has been applied at Microsoft in the internal development process. Though a success story compared to other formal quality assurance approaches like verification, a break-through of the technology on a broader scale is not in sight. What are the obstacles? Some lessons can be learned from the past and will be discussed. An approach to MBT is described which is based on modeling, which gives users the freedom to choose among programmatic and diagrammatic notations, as well as state-based and scenario-based (interaction-based) styles, reflecting the different concerns in the process. The diverse model styles can be combined by model composition in order to achieve an integrated and collaborative model-based testing process. The approach is realized in the successor of Microsoft Research’s MBT tool Spec Explorer, and has a formal foundation in the framework of action machines.

A observes the sequence of events in a system, and takes appropriate action when a given pattern occurs in that sequence. Aspect-oriented programming provides a convenient framework for writing such trace monitors.

We provide a brief introduction to aspect-oriented programming in AspectJ. AspectJ only provides support for triggering extra code with single events, and we present a new language feature (named ) that allows one to directly express patterns that range over the whole current trace. Implementing this feature efficiently is challenging, and we report on our work towards that goal.

Another drawback of AspectJ is the highly syntactic nature of the event patterns, often requiring the programmer to list all methods that have a certain property, rather than specifying that property itself. We argue that provides an appropriate notation for describing such properties. Furthermore, all of the existing patterns in AspectJ can be reduced to Datalog via simple rewrite rules.

This research is carried out with , an extensible optimising compiler for AspectJ, which is freely available for download.

The starting point for Model-Based Testing is an implementation relation that formally defines when a formal model representing the System Under Test conforms to a formal model constituting its specification. An implementation relation for the formalism of Labelled Transition Systems is . For several test generation algorithms and test tools have been built. In this paper we define a framework for the symbolic implementation relation which lifts to Symbolic Transition Systems. These are transition systems with an explicit notion of data and data-dependent control flow. The introduction of symbolism avoids the state-space explosion during test generation, and it preserves the information present in data definitions and constraints for use during the test selection process. We show the soundness and completeness of the symbolic notions w.r.t. their underlying Labelled Transition Systems’ counterparts.

We propose a syntax-driven test generation technique to automaticaly derive abstract test cases from a set of requirements expressed in a linear temporal logic. Assuming that an elementary test case (called a“tile”) is associated to each basic predicate of the formula, we show how to generate a set of test controlers associated to each logical operator, and able to coordinate the whole test execution. The test cases produced are expressed in a process algebraic style, allowing to take into account the test environment constraints. We illustrate this approach in the context of network security testing, for which more classical model-based techniques are not always suitable.

Input-output conformance test theory for discrete systems has established itself in research and industry already. A couple of years ago also input-output conformance test theories for timed systems were defined. The next step is to develop conformance test theory for hybrid systems as well. In this paper we present a conformance relation for model-based testing of hybrid systems and we formalize tests for hybrid systems.

We present a way to generate test sequences from EFSM models using a guided model checker: Uppaal Cora. The approach allows to specify various structural test coverage criteria of EFSMs, for example, selected states/transitions, all transitions, all transition pairs, etc. We describe a method to construct Uppaal models to achieve test sequences satisfying these criteria and experiment with the search options of Uppaal to achieve test sequences that are suboptimal in terms of length. We apply a bitstate hashing space reduction based iterated search refinement method to shorten the length of test sequences with respect to the length gained using depth first search. The test generation method and different search strategies are compared by applying them on a stopwatch and INRES protocol based case study. The outcome shows the feasibility of applying guided model checking in conjunction with iterated search refinement for generating suboptimal test sequences.

To efficiently solve safety verification and testing problems for an aspect-oriented system, we use multitape automata to model aspects and propose algorithms for the aspect-oriented system specified by a number of primary labeled transition systems (some of them are black-boxes) and aspects. Our algorithms combine automata manipulations over the aspects and primary systems with black-box testing over each individual black-box, but without generating the woven system.

In this paper we present a novel automated, on-line, modelbased testing system for on-the-fly testing of thin-client web applications. Web applications are specified by means of Extended State Machines. To handle dynamic web applications, arbitrarily large and complex state input and output types, and the transport of information from the webpage to the state of the specification, we define a new, ioco like, conformance relation. In this conformance relation a specification is a function from state and input to functions from output to the new states. The implementation builds on the G∀ST test tool and spots errors in real web applications.

When models are formal, model based testing approaches usually construct a coverage graph through symbolic execution and derive test cases in the form of paths in the coverage graph. Thereafter consistency between the model and the implementation is verified in relation to the test cases. Existing approaches, especially when dealing with model oriented languages like B, partition the input space of each operation in the model to create operation instances, and then animate the model in relation to these instances. The paths or the test cases are now a sequence of operation instances. However, in this approach, there is no guarantee that we test the user scenarios. In this paper, we first define scenario based test cases in relation to the initial specification. When this specification passes through a succession of refinements, we derive scenario based test cases for each refinement and show that all these test cases are equivalent to the test cases of the original specification.

A well-established theory exists for testing finite-state machines, in particular Moore and Mealy machines. A fundamental class of problems handled by this theory is state identification: we are given a machine with known state space and transition relation but unknown initial state, and we are asked to find experiments which permit to identify the initial or final state of the machine, called distinguishing and homing experiments, respectively.

In this paper, we study state-identification for finite-state transducers. The latter are a generalization of Mealy machines where outputs are sequences rather than symbols. Transducers permit to model systems where inputs and outputs are not synchronous, as is the case in Mealy machines. It is well-known that every deterministic and minimal Mealy machine admits a homing experiment. We show that this property fails for transducers, even when the latter are deterministic and minimal. We provide answers to the decidability question, namely, checking whether a given transducer admits a particular type of experiment. First, we show how the standard successor-tree algorithm for Mealy machines can be turned into a semi-algorithm for transducers. Second, we show that the state-identification problems are undecidable for finite-state transducers in general. Finally, we identify a sub-class of transducers for which these problems are decidable. A transducer in this sub-class can be transformed into a Mealy machine, to which existing methods apply.