FATES-RV on Tuesday, August 15th

Session 1: Invited Talk (09:00‑10:00)

09:00‑10:00

Wolfgang Grieskamp (Microsoft Research, USA) Multi-Paradigmatic Model-Based Testing [ppt] 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 multi-paradigmatic modeling, which gives users the freedom to choose among programmatic and diagrammatic notations, as well as state-based and scenario-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. See tool website.

Break (10:00‑10:30)

Session 2 (10:30‑12:30)

10:30‑11:00	Lars Frantzen (Radboud University Nijmegen) Jan Tretmans (Radboud University Nijmegen) Tim Willemse (Radboud University Nijmegen) A Symbolic Framework for Model-Based Testing 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 ioco. For ioco several test generation algorithms and test tools have been built. In this paper we define a framework for the symbolic implementation relation sioco which lifts ioco 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.
11:00‑11:30	Jean-Claude Fernandez (VERIMAG/Université Joseph Fourier de Grenoble) Laurent Mounier (VERIMAG/Université Joseph Fourier de Grenoble) Jean-luc Richier (LSR/Université Joseph Fourier de Grenoble) A Test Calculus Framework Applied to Network Security Policies 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.
11:30‑12:00	Michiel van Osch (Technische Universiteit Eindhoven) Hybrid Input-output Conformance and Test Generation 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.
12:00‑12:30	Juhan P. Ernits (Inst. of Cybernetics / Dept. of Comp. Sci., Tallinn University of Technology) Andres Kull (Elvior) Kullo Raiend (Elvior) Jüri Vain (Dept. of Comp. Sci. / Inst. of Cybernetics, Tallinn University of Technology) Generating Tests from EFSM Models using Guided Model Checking and Iterated Search Refinement 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 the 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.

Lunch break (12:30‑14:00)

Session 3 (14:00‑15:30)

14:00‑14:30	Cheng Li (Washington State University) zhe dang (washington state university) Decompositional Algorithms for Safety Verification and Testing of Aspect-Oriented Systems To 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.
14:30‑15:00	Pieter Koopman (Radboud University Nijmegen) Rinus Plasmeijer (Radboud University Nijmegen) Peter Achten (Radboud University Nijmegen) Model-Based Testing of Thin-Client Web Applications In this paper we present a novel automated, on-line, model-based 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 web-page 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 gast test tool and spots errors in real web applications.
15:00‑15:30	Manoranjan Satpathy (Abo Akademi) Qaiser Malik (Abo Akademi) Johan Lilius (Abo Akademi) Synthesis of Scenario Based Test Cases from B Models When model 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 thereafter animate the model in relation to them. 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 initially define what the scenario based test cases are and then synthesize such test cases across refinements. In the process, we define scenario-based test cases for each refinement. Usually the implementation is written in accordance with a refinement, and if the implementation is tested against the test cases of this refinement, we can conclude that the implementation has been tested for its scenarios.

Break (15:30‑16:00)

Session 4: Tool Demos (16:00‑17:30)