nach oben

2014 | Buch

Kapitel lesen Erstes Kapitel lesen

Tests and Proofs

8th International Conference, TAP 2014, Held as Part of STAF 2014, York, UK, July 24-25, 2014. Proceedings

herausgegeben von: Martina Seidl, Nikolai Tillmann

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the refereed proceedings of the 8th International Conference on Tests and Proofs, TAP 2014, held in York, UK, in July 2014, as part of the STAF 2014 Federated Conferences. The 10 revised full papers and 4 short papers presented together with two tutorial descriptions were carefully reviewed and selected from 27 submissions. The papers cover topics in the following four research areas: test generation, bridging semantic gaps, integrated development processes and bounded verification.

Inhaltsverzeichnis

Frontmatter

Model-Based Mutation Testing of an Industrial Measurement Device

Abstract

MoMuT::UML is a model-based mutation testing tool for UML models. It maps UML state machines to a formal semantics and performs a conformance check between an original and a set of mutated models to automatically generate test cases. The resulting test suite is able to detect whether a system under test implements one of the faulty models instead of the correct, original model. In this work, we illustrate the whole model-based mutation testing process by means of an industrial case study. We test the control logic of a device that counts the particles in exhaust gases. First, we model the system under test in UML. Then, MoMuT::UML is used to automatically generate three test suites from the UML test model: one mutation-based test suite, one set of random test cases, and a third test suite combining random and mutation-based test case generation. The test cases are executed on the system under test and effectively reveal several errors. Finally, we compare the fault detection capabilities of the three test suites on a set of faulty systems, which were created by intentionally injecting faults into the implementation.

Bernhard K. Aichernig, Jakob Auer, Elisabeth Jöbstl, Robert Korošec, Willibald Krenn, Rupert Schlick, Birgit Vera Schmidt

Computing with an SMT Solver

Abstract

Satisfiability modulo theories (SMT) solvers that support quantifier instantiations via matching triggers can be programmed to give practical support for user-defined theories. Care must be taken to avoid so-called matching loops, which may prevent termination of the solver. By design, such avoidance limits the extent to which the SMT solver is able to apply the definitions of user-defined functions. For some inputs to these functions, however, it is instead desireable to allow unadulterated use of the functions; in particular, if it is known that evaluation will terminate.

This paper describes the program verifier Dafny’s SMT encoding of recursive user-defined functions. It then describes a novel encoding that, drawing on ideas from offline partial evaluation systems, lets the SMT solver evaluate “safe” function applications while guarding against matching loops for others.

Nada Amin, K. Rustan M. Leino, Tiark Rompf

An Abstraction Technique for Testing Decomposable Systems by Model Checking

Abstract

Test generation by model checking exploits the capability of model checkers to return counterexamples upon property violations. The approach suffers from the state explosion problem of model checking. For property verification, different abstraction techniques have been proposed to tackle this problem. However, such techniques are not always suitable for test generation. In this paper we focus on Decomposable by Dependency Asynchronous Parallel (DDAP) systems, composed by several subsystems running in parallel and connected together in a way that the inputs of one subsystem are provided by another subsystem. We propose a test generation approach for DDAP systems based on a decompositional abstraction that considers one subsystem at a time. It builds tests for the single subsystems and combines them later in order to obtain a global system test. Such approach avoids the exponential increase of the test generation time and memory consumption. The approach is proved to be sound, but not complete.

Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene

An All-in-One Toolkit for Automated White-Box Testing

Abstract

Automated white-box testing is a major issue in software engineering. Over the years, several tools have been proposed for supporting distinct parts of the testing process. Yet, these tools are mostly separated and most of them support only a fixed and restricted subset of testing criteria. We describe in this paper Frama-C/LTest, a generic and integrated toolkit for automated white-box testing of C programs. LTest provides a unified support of many different testing criteria as well as an easy integration of new criteria. Moreover, it is designed around three basic services (test coverage estimation, automatic test generation, detection of uncoverable objectives) covering most major aspects of white-box testing and taking benefit from a combination of static and dynamic analyses. Services can cooperate through a shared coverage database. Preliminary experiments demonstrate the possibilities and advantages of such cooperations.

Sébastien Bardin, Omar Chebaro, Mickaël Delahaye, Nikolai Kosmatov

Behaviour Driven Development for Tests and Verification

Abstract

The design of hardware systems is a challenging and error-prone task, where a signifcant portion of the effort is spent for testing and verification. Usually testing and verification are applied as a post-process to the implementation. Meanwhile, for the development of software, test-first approaches such as test driven development (TDD) have become increasingly important. In this paper, we propose a new design flow based on behaviour driven development (BDD), an extension of TDD, where acceptance tests written in natural language drive the implementation. We extend this idea by allowing the specification of properties in natural language and use them as a starting point in the design flow. The flow also includes an automatic generalisation of test cases to properties that are used for formal verification. In this way, testing and formal verification are combined in a seamless manner, while keeping the requirements — from which both tests and formal properties are derived — in a single consistent document. The approach has been implemented and evaluated on several examples to demonstrate the advantages of the proposed flow.

Melanie Diepenbeck, Ulrich Kühne, Mathias Soeken, Rolf Drechsler

Quality Assurance in MBE Back and Forth

Abstract

The maturing of model-based engineering (MBE) has led to an increased interest and demand on the verification of MBE artifacts. Numerous verification approaches have been proposed in the past and, in fact, due to their diversity it is sometimes difficult to determine whether a suitable approach for the verification task at hand exists. In the first part of this tutorial, we thus present a classification for verification approaches of MBE artifacts that allows us to categorize approaches, among others, according to their intended verification goal and the capabilities of their verification engine. Based thereon, we briefly overview the landscape of existing verification approaches. In the second part, we iteratively build and verify the behavioral correctness of a small software system with our OCL-based model checker MocOCL..

Sebastian Gabmeyer

Visualizing Unbounded Symbolic Execution

Abstract

We present an approach for representing and visualizing all possible symbolic execution paths of a program. This is achieved by integrating method contracts and loop invariants into a symbolic execution engine and rendering them visually in a suitable manner. We use the technique to create an omniscient visual symbolic state debugger for Java that can deal with unbounded loops and method calls.

Martin Hentschel, Reiner Hähnle, Richard Bubel

Filmstripping and Unrolling: A Comparison of Verification Approaches for UML and OCL Behavioral Models

Abstract

Guaranteeing the essential properties of a system early in the design process is an important as well as challenging task. Modeling languages such as the UML allow for a formal description of structure and behavior by employing OCL class invariants and operation pre- and postconditions. This enables the verification of a system description prior to implementation. For this purpose, first approaches have recently been put forward. In particular, solutions relying on the deductive power of constraint solvers are promising. Here, complementary approaches of how to formulate and transform respective UML and OCL verification tasks into corresponding solver tasks have been proposed. However, the resulting methods have not yet been compared to each other. In this contribution, we consider two verification approaches for UML and OCL behavioral models and compare their methods and the respective workflows with each other. By this, a better understanding of the advantages and disadvantages of these verification methods is achieved.

Frank Hilken, Philipp Niemann, Martin Gogolla, Robert Wille

Generating Classified Parallel Unit Tests

Abstract

Automatic generation of parallel unit tests is an efficient and systematic way of identifying data races inside a program. In order to be effective parallel unit tests have to be analysed by race detectors. However, each race detector is suitable for different kinds of race conditions. This leaves the question which race detectors to execute on which unit tests. This paper presents an approach to generate classified parallel unit tests: A class indicates the suitability for race detectors considering low-level race conditions, high-level atomicity violations or race conditions on correlated variables. We introduce a hybrid approach for detecting endangered high-level atomic regions inside the program under test. According to these findings the approach classifies generated unit tests as low-level, atomic high-level or correlated high-level. Our evaluation results confirmed the effectiveness of this approach. We were able to correctly classify 83% of all generated unit tests.

Ali Jannesari, Nico Koprowski, Jochen Schimmel, Felix Wolf

JTACO: Test Execution for Faster Bounded Verification

Abstract

In bounded program verification a finite set of execution traces is exhaustively checked in order to find violations to a given specification (i.e. errors). SAT-based bounded verifiers rely on SAT-Solvers as their back-end decision procedure, accounting for most of the execution time due to their exponential time complexity.

In this paper we sketch a novel approach to improve SAT-based bounded verification. As modern SAT-Solvers work by augmenting partial assignments, the key idea is to translate some of these partial assignments into JUnit test cases during the SAT-Solving process. If the execution of the generated test cases succeeds in finding an error, the SAT-Solver is promptly stopped.

We implemented our approach in JTACO, an extension to the TACO bounded verifier, and evaluate our prototype by verifying parameterized unit tests of several complex data structures.

Alexander Kampmann, Juan Pablo Galeotti, Andreas Zeller

Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification

Abstract

Formal modular verification of software is based on assume-guarantee reasoning, where each software module is shown to provide some guarantees under certain assumptions and an overall argument linking results for individual modules justifies the correctness of the approach. However, formal verification is almost never applied to the entire code, posing a potential soundness risk if some assumptions are not verified. In this paper, we show how this problem was addressed in an industrial project using the SPARK formal verification technology, developed at Altran UK. Based on this and similar experiences, we propose a partial automation of this process, using the notion of explicit assumptions. This partial automation may have the role of an enabler for formal verification, allowing the application of the technology to isolated modules of a code base while simultaneously controlling the risk of invalid assumptions. We demonstrate a possible application of this concept for the fine-grain integration of formal verification and testing of Ada programs.

Johannes Kanig, Rod Chapman, Cyrille Comar, Jerôme Guitton, Yannick Moy, Emyr Rees

A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing

Abstract

Complete formal verification of software remains extremely expensive and often reserved in practice for the most critical products. Test generation techniques are much less costly and can be used in combination with theorem proving tools to provide high confidence in the software correctness at an acceptable cost when an automatic prover does not succeed alone. This short paper presents a case study on verification of a cloud hypervisor with the Frama-C toolset, in which deductive verification has been advantageously combined with structural all-path testing. We describe our combined verification approach, present the adopted methodology and emphasize its benefits and limitations.

Nikolai Kosmatov, Matthieu Lemerre, Céline Alec

Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses

Tutorial Synopsis

Abstract

Among various static and dynamic software verification techniques, runtime assertion checking traditionally holds a particular place. Commonly used by most software developers, it can provide a fast feedback on the correctness of a property for one or several concrete executions of the program. Quite easy to realize for simple program properties, it becomes however much more complex for complete program contracts written in an expressive specification language. This paper presents a one-hour tutorial on runtime assertion checking in which we give an overview of this popular dynamic verification technique, present its various combinations with other verification techniques (such as static analysis, deductive verification, test generation, etc.) and emphasize the benefits and difficulties of these combinations. They are illustrated on concrete examples of C programs within the Frama-C software analysis framework using the executable specification language E-ACSL.

Nikolai Kosmatov, Julien Signoles

Generating Test Data from a UML Activity Using the AMPL Interface for Constraint Solvers

Abstract

Testing is one of the most wide-spread means for quality assurance. Modelling and automated test design are two means to improve effectivity and efficiency of testing. In this paper, we present a method to generate test data from UML activity diagrams and OCL constraints by combining symbolic execution and state–of–the–art constraint solvers. Our corresponding prototype implementation is integrated in the existing test generator ParTeG and generates C++ unit tests. Our key improvement is the transparent use of multiple industry strength solvers through a common interface; this allows the user to choose between an expressive constraint language or highly optimised test data generation. We use infeasible path elimination to improve the performance of test generation and boundary value analysis to improve the quality of the generated test data. We provide an industrial case study and measure the performance of our tool using different solvers in several scenarios.

Felix Kurth, Sibylle Schupp, Stephan Weißleder

Lightweight State Capturing for Automated Testing of Multithreaded Programs

Abstract

We present a lightweight approach to capture abstract state information that can be used to avoid testing redundant interleavings of multithreaded programs. Our approach is based on modeling states that are observed during the test executions as a Petri net. This model is then used to determine if some execution paths lead to an already explored state. In such cases exploring execution paths from the same state multiple times can be avoided. Our approach does not capture the complete global states of programs but instead it relies on particular commutativity of transitions to determine if they lead to already known abstract states. We have combined this lightweight state capture technique with a dynamic symbolic execution based approach to systematically test multithreaded programs. Experiments show that even without complete state information, the lightweight state capturing technique can sometimes reduce the number of redundant test executions substantially.

Kari Kähkönen, Keijo Heljanko

How Test Generation Helps Software Specification and Deductive Verification in Frama-C

Abstract

This paper describes an incremental methodology of deductive verification assisted by test generation and illustrates its benefits by a set of frequent verification scenarios. We present StaDy, a new integration of the concolic test generator PathCrawler within the software analysis platform Frama-C . This new plugin treats a complete formal specification of a C program during test generation and provides the validation engineer with a helpful feedback at all stages of the specification and verification tasks.

Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand

Backmatter

Titel: Tests and Proofs
herausgegeben von: Martina Seidl
Nikolai Tillmann
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-09099-3
Print ISBN: 978-3-319-09098-6
DOI: https://doi.org/10.1007/978-3-319-09099-3

Springer Professional

Über dieses Buch

Inhaltsverzeichnis

Frontmatter

Model-Based Mutation Testing of an Industrial Measurement Device

Computing with an SMT Solver

An Abstraction Technique for Testing Decomposable Systems by Model Checking

An All-in-One Toolkit for Automated White-Box Testing

Behaviour Driven Development for Tests and Verification

Quality Assurance in MBE Back and Forth

Visualizing Unbounded Symbolic Execution

Filmstripping and Unrolling: A Comparison of Verification Approaches for UML and OCL Behavioral Models

Generating Classified Parallel Unit Tests

JTACO: Test Execution for Faster Bounded Verification

Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification

A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing

Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses

Generating Test Data from a UML Activity Using the AMPL Interface for Constraint Solvers

Lightweight State Capturing for Automated Testing of Multithreaded Programs

How Test Generation Helps Software Specification and Deductive Verification in Frama-C

Backmatter

Premium Partner