calame.de - Publications

2014

2008

Software faults are a well-known phenomenon. In most cases, they are just annoying - if the computer game does not work as expected - or expensive - if once again a space project fails due to some faulty data conversion. In critical systems, however, faults can have life-threatening consequences. It is the task of software quality assurance to avoid such faults, but this is a cumbersome, expensive and also erroneous undertaking. For this reason, research has been done over the last years in order to automate this task as much as possible.
In this thesis, the connection of constraint solving techniques with formal methods is investigated. We have the goal to find faults in the models and implementations of reactive systems with data, such as automatic teller machines (ATMs). In order to do so, we first develop a translation of formal specifications in the process algebra µCRL to a constraint logic program (CLP). In the course of this translation, we pay special attention on the fact that the CLP together with the constraint solver correctly simulates the underlying term rewriting system.
One way to validate a system is the test whether this system conforms its specification. In this thesis, we develop a test process to automatically generate and execute test cases for the conformance test of data-oriented systems. The applicability of this process to process-oriented software systems is demonstrated in a case study with an ATM as the system under test. The applicability of the process to document-centered applications is shown by means of the open source web browser Mozilla Firefox.
The test process is partially based on the tool TGV, which is an enumerative test case generator. It generates test cases from a system specification and a test purpose. An enumerative approach to the analysis of system specifications always tries to enumerate all possible combinations of values for the system's data elements, i.e. the system's states. The states of those systems, which we regard here, are influenced by data of possibly infinite domains. Hence, the state space of such systems grows beyond all limits, it explodes, and cannot be handled anymore by enumerative algorithms. For this reason, the state space is limited prior to test case generation by a data abstraction. We use a chaotic abstraction here with all possible input data from a system's environment being replaced by a single constant.
In parallel, we generate a CLP from the system specification. With this CLP, we reintroduce the actual data at the time of test execution. This approach does not only limit the state space of the system, but also leads to a separation of system behavior and data. This allows to reuse test cases by only varying their data parameters.
In the developed process, tests are executed by the tool BAiT. This tool has also been created in the course of this thesis. Some systems do not always show an identical behavior under the same circumstances. This phenomenon is known as nondeterminism. There are many reasons for nondeterminism. In most cases, input from a system's environment is asynchronously processed by several components of the system, which do not always terminate in the same order. BAiT works as follows: The tool chooses a trace through the system behavior from the set of traces in the generated test cases. Then, it parameterizes this trace with data and tries to execute it. When the nondeterministic system digresses from the selected trace, BAiT tries to appropriately adapt it. If this can be done according to the system specification, the test can be executed further and a possibly false positive test verdict has been successfully avoided.
The test of an implementation significantly reduces the numbers of faults in a system. However, the system is only tested against its specification. In many cases, this specification already does not completely fulfill a customer's expectations. In order to reduce the risk for faults further, the models of the system themselves also have to be verified. This happens during model checking prior to testing the software. Again, the explosion of the state space of the system must be avoided by a suitable abstraction of the models.
A consequence of model abstractions in the context of model checking are so-called false negatives. Those traces are counterexamples which point out a fault in the abstracted model, but who do not exist in the concrete one. Usually, these false negatives are ignored. In this thesis, we also develop a methodology to reuse the knowledge of potential faults by abstracting the counterexamples further and deriving a violation pattern from it. Afterwards, we search for a concrete counterexample utilizing a constraint solver.
Conformance testing is a widely used approach to validate a system correct w.r.t. its specification. This approach is mainly used for behavior-oriented systems. BAiT (Behavior Adaptation in Testing) is a conformance testing approach for data-intensive reactive systems. In this paper, we validate the applicability of BAiT to systems, which are not behavior-oriented (reactive) but document-centered. In particular, we apply BAiT to the test of the HTML rendering engine Gecko, which is used by Mozilla Firefox. In order to do so, we formally specify a part of the CSS box model in the specification language µCRL and implement a wrapper for the Gecko renderer. Then, we automatically generate test cases and run tests with BAiT in a controlled experiment in order to demonstrate our approach on the relevant part of Gecko.
Download

2007

Safe data abstractions are widely used for verification purposes. Positive verification results can be transferred to the concrete system. When a property is violated in the abstract system, one still has to check whether a concrete violation exists. However, even when the violation scenario is not reproducible in the concrete system (a false negative), it may still contain information on possible sources of bugs. Here we propose a bug hunting framework based on abstract violation scenarios. We first extract a violation pattern from an abstract violation scenario. The violation pattern represents multiple violation scenarios, increasing the chance that a corresponding concrete violation exists. Then we look for a concrete violation that corresponds to the violation pattern by using constraint solving techniques. Finally, we define the class of counterexamples that we can handle and argue correctness of the proposed framework. Our method combines two formal techniques, model checking and constraint solving. Through an analysis of contracting and precise abstractions, we are able to integrate overapproximation by abstraction with concrete counterexample generation.
Developing test suites is a costly and error-prone process. Model-based test generation tools facilitate this process by automatically generating test cases from system models. The applicability of these tools, however, depends on the size of the target systems. Here, we propose an approach to generate test cases by combining data abstraction, enumerative test generation and constraint-solving. Given the concrete specification of a possibly infinite system, data abstraction allows to derive an abstract system, which is finite and thus suitable for the automatic generation of abstract test cases with enumerative tools. To execute abstract test cases, we have to instantiate them with concrete data. For data selection we make use of constraint-solving techniques.
Behavior-oriented Adaptation in Testing (BAiT) is a toolset, which supports test generation and execution for deterministic and nondeterministic systems with data. It covers the generation of test cases from a (formal) system specification and test purposes, the identification and selection of test data during test execution and, where necessary and possible, the dynamic adaptation of a test run to the reactions of the implementation under test. The test generation part of the toolset is based on the tool Test Generation with Verification Techniques (TGV) from the Caesar/Aldébaran Development Package (CADP).
Safe data abstractions are widely used for verification purposes. Positive verification results can be transferred from the abstract to the concrete system. When a property is violated in the abstract system, one still has to check whether a concrete violation scenario exists. However, even when the violation scenario is not reproducible in the concrete system (a false negative), it may still contain information on possible sources of bugs. Here, we propose a bug hunting framework based on abstract violation scenarios. We first extract a violation pattern from one abstract violation scenario. The violation pattern represents multiple abstract violation scenarios, increasing the chance that a corresponding concrete violation exists. Then, we look for a concrete violation that corresponds to the violation pattern by using constraint solving techniques. Finally, we define the class of counterexamples that we can handle and argue correctness of the proposed framework. Our method combines two formal techniques, model checking and constraint solving. Through an analysis of contracting and precise abstractions, we are able to integrate overapproximation by abstraction with concrete counterexample generation.
Download
Models in process algebra with abstract data types can be analysed by state space generation and reduction tools. The µCRL toolset implements a suite of distributed verification tools for clusters of workstations. We illustrate their application to large case studies from a wide range of application areas, such as functional analysis, scheduling, security analysis, test case generation and game solving.
Download

2006

Der Test von Software ist ein notwendiges, jedoch ressourcenintensives Unterfangen. Aus diesem Grund wurden verschiedene Ansätze entwickelt, die einzelnen Aspekte des Softwaretests zu automatisieren. In diesem Paper stellen wir einen Ansatz zur automatischen Testfallerzeugung für den modellbasierten Test vor. Dabei werden aus UML-Modellen eines Softwaresystems und der Beschreibung von Testszenarien parametrisierbare Testfälle in TTCN-3 erzeugt. Die Parametrisierung erhöht dabei die Wiederverwendbarkeit der Testfälle, unterstützt die gezielte Auswahl geeigneter Testdaten und wirkt so dem Phänomen der Testfallexplosion entgegen.
Safe data abstractions are widely used for verification purposes. Positive verification results can be transferred to the concrete system. When a property is violated in the abstract system, one still has to check whether a concrete violation exists. However, even when the violation scenario is not reproducible in the concrete system (a false negative), it may still contain information on possible sources of bugs. Here we propose a bug hunting framework based on abstract violation scenarios. We first extract a violation pattern from an abstract violation scenario. The violation pattern represents multiple violation scenarios, increasing the chance that a corresponding concrete violation exists. Then we look for a concrete violation that corresponds to the violation pattern by using constraint solving techniques.
Railway control systems are safety-critical, so we have to ensure that they are designed and implemented correctly. Testing these systems is a key issue. Prior to system testing, the software of a railway control system is tested separately from the hardware. The interlocking is a layer of railway control systems that guarantees safety. It allows to execute commands given by a user only if they are safe; unsafe commands are rejected. Railway interlockings are central to efficient and safe traffic management for railway infrastructure managers and operators. European integration requires new standards for specification and testing interlockings. Here we propose an approach to testing interlockings with TTCN-3 and give an example for its application. The code of interlockings is simulated during test execution. For assessing the quality of the tests, we propose an approach inspired by the Classification Tree Method.
Download
Testing modern software-intensive systems is a complex process that often lacks proper means for management and documentation. In this paper, we propose an approach to specifying and documenting a test process framework that facilitates automatization of testing processes. The approach bridges the gap between product requirements, software under test, and the actual testware. It also allows to specify stages of a specific test process. We use Meta Object Facility-based meta models as the specification basis for our approach. Furthermore, we provide an application of the approach to testing connector-based multi agent systems.
Model-based tools for automatic test generation usually can handle systems of a rather limited size. Therefore, they cannot be applied directly to systems of real industrial size. Here, we propose an approach to test generation combining enumerative data abstraction, test generation methods and constraint solving. The approach allows applying enumerative test generation tools like TGV to large and infinite systems. Given such a system, abstractions allow to derive a finite abstract system suitable for automatic test generation with enumerative tools. Abstract test cases need to be parameterized with actual test data, in order to execute them. For data selection, we make use of constraint solving techniques. Test case execution will later be done by TTCN-3.

2005

Conformance testing is one of the most rigorous and well-developed testing techniques. Model-based test generation is an essential phase of the conformance testing approach. The main problem in this phase is the explosion of the number of test cases, often caused by large or infinite data domains for input and output data. In this paper we propose a test generation framework based on the use of data abstraction and constraint solving to suppress the number of test cases. The approach is evaluated on the CEPS (Common Electronic Purse Specifications) case study.
Download
TGV (Test Generation with Verification technology) is a tool, integrated into the toolset CADP, for the generation of test cases based on a system's specification and a test purpose. In this report we discuss the integration of µCRL and TGV into the process of test generation. We also work out the ioco theory and its relation to TGV. Furthermore, we do not only discuss the theoretical aspects of the tool itself, but also its practical usage.

2004

.NET Remoting ist eines der führenden Entwicklungsframeworks für die Erstellung verteilter Systeme. Dieses Buch erklärt Ihnen umfassend und gut verständlich alle relevanten technologischen Aspekte von .NET Remoting und ermöglicht Ihnen die Erstellung von leistungsfähigen und skalierbaren verteilten Systemen.
Die Autoren führen Sie zunächst in die Besonderheiten verteilter Systeme ein. Darauf aufbauend werden detailliert die Konzepte und Technologien erläutert: von der verteilten Objektkonstruktion über Persistenz, Konfiguration und Deployment, synchrone und asynchrone Kommunikation bis hin zu Sicherheitsaspekten. Zu all diesen Themen finden Sie ein durchgängiges Beispiel, das in den abschließenden Kapiteln zu einer umfassenden Anwendung ausgebaut wird. Weiterhin wagen die Autoren einen Blick in die Zukunft und geben Ihnen Hinweise, wie Sie Ihre Anwendungen mit Hinblick auf Indigo zukunftssicher gestalten können. Eine Referenz der wichtigsten APIs und der verwendeten Patterns rundet das Buch ab. Alle Kapitel sind so aufgebaut, dass lineares Lesen und Querlesen gleichermaßen möglich ist. Damit eignet sich das Buch sowohl als Leitfaden für .NET Remoting Einsteiger als auch als konzeptionelles Referenzwerk für Fortgeschrittene.
Diese Arbeit beschäftigt sich mit dem Test ADE-basierter Multiagentensysteme. Zunächst wird ein System aus Metastrukturen zur Beschreibung eines allgemeinen Testverfahrens entwickelt. Darauf aufbauend wird ein Patternkatalog für den Test von Multiagentensystemen aufgestellt sowie ein Testframework entwickelt und vorgefertigt. Patternkatalog und Testframework werden abschließend anhand eines Beispielszenariums evaluiert.

2003

This work deals with object oriented software testing. It does not only focus on the modular part of testing but also on the analysis of object oriented program structures and adequate tests, which also regard such principles as data hiding and polymorphy, and the resulting problems for inspecting the states of objects. The modular part of object oriented testing is represented by a meta structure as an abstraction of common unit testing frameworks.