Computer Science Colloquium
Cyrille Artho und Takashi Kitamura
Senior Researcher und Post-doctorial research scientist at AIST, Japan
Modbat: A Model-based API Tester for Event-driven Systems und Test-Case Design by Feature Trees
Tue 10.09.2013, 10:00, 120 minutesSP3 218
Abstract
Abstract 1:Model-based testing derives test executions from an abstract model that describes the system behavior. However, existing approaches are not tailored to event-driven or input/output-driven systems. In particular, there is a need to support non-blocking I/O operations, or operations throwing exceptions when communication is disrupted.
Our new tool "Modbat" is specialized for testing systems where these issues are common. Modbat uses extended finite-state machines to model system behavior. Unlike most existing tools, Modbat offers a domain-specific language that supports state machines and exceptions as first-class constructs. Our model notation also handles non-determinism in the system under test, and supports alternative continuations of test cases depending on the outcome of non-deterministic operations.These features allow us to model a number of interesting libraries succinctly. Our experiments show the flexibility of Modbat and how language support for model features benefits their correct use.
Abstract 2:
We propose a test-case design method for black-box testing, called "Feature Oriented Testing (FOT)". The method is realized by applying Feature Models (FMs) developed in software product line engineering to test-case designs. We develop a graphical language for test-case design called "Feature Trees for Testing (FTT)" based on FMs. To firmly underpin the method, we provide a formal semantics of FTT, by means of test-cases derived from test-case designs modeled with FTT. Based on the semantics we develop an automated test-suite generation and correctness checking of test-case designs using SAT, as computer-aided analysis techniques of the method. Feasibility of the method is demonstrated from several viewpoints including its implementation, complexity analysis, experiments, a case study, and an assistant tool.
Bio
Cyrille Artho obtained his Ph.D. at ETH Zurich, Switzerland, in 2005. After his Ph.D., he moved to NII, Tokyo, Japan, to continue his research, and is now a Senior Researcher at AIST, where he has been working since 2007.Cyrille Artho's main interests are software verification and software engineering. In his master's thesis, he compared different approaches for finding faults in multi-threaded programs. Later in his Ph.D. thesis, he continued his search for such errors, while also looking at test case generation. His most recent work focuses on analyzing networked systems.
Takashi Kitamura obtained his ph.D. from the Chinese Academy of Sciences, Beijing, in 2008. Since then, he has been working at AIST, Amagasaki, Japan, as a post-doctoral researcher and later as research scientist. His interests include the formal analysis of requirements and formal, model-based approaches to testing. His most recent work focuses on combinatorial approaches to test case generation.
Invited by Prof. Dr. Armin Biere, Institut für Formale Modelle und Verifikation
The Computer Science Colloquium is organized by the Department of Coputer Science at JKU, the Österreichische Gesellschaft für Informatik (ÖGI) and the Österreichische Computergesellschaft (OCG).