nach oben

2019 | Buch

Kapitel lesen Erstes Kapitel lesen

Tests and Proofs

13th International Conference, TAP 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9–11, 2019, Proceedings

herausgegeben von: Dirk Beyer, Chantal Keller

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

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

Inhaltsverzeichnis

Über dieses Buch

This book constitutes the refereed proceedings of the 13th International Conference on Tests and Proofs, TAP 2019, held as part of the Third World Congress on Formal Methods 2019, Porto, Portugal, in October 2019.
The 10 regular papers and 2 invited paper presented in this volume were carefully reviewed and selected from 19 submissions. The TAP conference promotes research in verification and formal methods that targets the interplay of proofs and testing: the advancement of techniques of each kind and their combination, with the ultimate goal of improving software and system dependability.

Inhaltsverzeichnis

Frontmatter

Invited Contributions

Frontmatter

When Are Software Verification Results Valid for Approximate Hardware?

Abstract

Approximate computing (AC) is an emerging paradigm for energy-efficient computation. The basic idea of AC is to sacrifice high precision for low energy by allowing hardware to carry out only “approximately correct” calculations. This provides a major challenge for software quality assurance: Programs successfully verified to be correct might be erroneous on approximate hardware.

In this paper, we present a novel approach for determining under what conditions a software verification result is valid for approximate hardware. To this end, we compute the allowed tolerances for AC hardware from successful verification runs. More precisely, we derive a set of constraints which – when met by the AC hardware – guarantee that the verification result carries over to AC. Our approach is based on the framework of abstract interpretation. Furthermore, we show (1) how to practically extract tolerances from verification runs employing predicate abstraction, and (2) how to check such constraints on hardware designs. We have implemented all techniques, and exemplify them on example C programs and a number of recently proposed approximate adders.

Tobias Isenberg, Marie-Christine Jakobs, Felix Pauck, Heike Wehrheim

Testing Robots Using CSP

Abstract

This paper presents a technique for automatic generation of tests for robotic systems based on a domain-specific notation called RoboChart. This is a UML-like diagrammatic notation that embeds a component model suitable for robotic systems, and supports the definition of behavioural models using enriched state machines that can feature time properties. The formal semantics of RoboChart is given using tock-CSP, a discrete-time variant of the process algebra CSP. In this paper, we use the example of a simple drone to illustrate an approach to generate tests from RoboChart models using a mutation tool called Wodel. From mutated models, tests are generated using the CSP model checker FDR. The testing theory of CSP justifies the soundness of the tests.

Ana Cavalcanti, James Baxter, Robert M. Hierons, Raluca Lefticaru

Regular Contributions

Frontmatter

Constraints in Dynamic Symbolic Execution: Bitvectors or Integers?

Abstract

Dynamic symbolic execution is a technique that analyses programs by gathering mathematical constraints along execution paths. To achieve bit-level precision, one must use the theory of bitvectors. However, other theories might achieve higher performance, justifying in some cases the possible loss of precision.

In this paper, we explore the impact of using the theory of integers on the precision and performance of dynamic symbolic execution of C programs. In particular, we compare an implementation of the symbolic executor KLEE using a partial solver based on the theory of integers, with a standard implementation of KLEE using a solver based on the theory of bitvectors, both employing the popular SMT solver Z3. To our surprise, our evaluation on a synthetic sort benchmark, the ECA set of Test-Comp 2019 benchmarks, and GNU Coreutils revealed that for most applications the integer solver did not lead to any loss of precision, but the overall performance difference was rarely significant.

Timotej Kapus, Martin Nowack, Cristian Cadar

Fast, Automatic, and Nearly Complete Structural Unit-Test Generation Combining Genetic Algorithms and Formal Methods

Abstract

Software testing is a time consuming and error prone activity, mostly manual in most industries. One approach to increase productivity is to automatically generate tests. In this paper, we focus on automatic generation of structural unit tests of safety-critical embedded software. Our purpose is to make a tool that integrates seamlessly with existing test processes in industry. We use genetic algorithms and automatic stub generation to quickly and automatically produce test cases satisfying test objectives of a given coverage criteria, using only the software under test as input. Moreover, we combine those genetic algorithms with formal methods to determine unfeasible test objectives and help on the coverage of difficult test objectives. We implemented our approach in a tool and tested it on a real-world industrial project, demonstrating that our approach can reliably generate test cases when feasible or demonstrate they are unfeasible for 99% of the MC/DC test objectives in about half an hour for 82,000 lines of C code with integer data.

Eric Lavillonnière, David Mentré, Denis Cousineau

Coverage-Based Testing with Symbolic Transition Systems

Abstract

We provide a model-based testing approach for systems comprising both state-transition based control flow, and data elements such as variables and data-dependent transitions. We propose test generation and execution, based on model-coverage: we generate test cases that aim to reach all transitions of the model. To obtain a test case reaching a certain transition, we need to combine reachability in the control flow, and satisfiability of the data elements of the model. Concrete values for data parameters are generated on-the-fly, i.e., during test execution, such that received outputs from the system can be taken into account for the inputs later provided in test execution. Due to undecidability of the satisfiability problem, SMT solvers may return result ‘unknown’. Our algorithm deals with this explicitly. We implemented our method in Maude combined with Z3, and use this to demonstrate the applicability of our method on the Bounded Retransmission Protocol benchmark. We measure performance by counting the number of inputs and outputs needed to discover bugs in mutants, i.e., in non-conforming variants of the specification. As a result, we find that we perform 3 times better, according to the geometric mean, than when using random testing as implemented by the tool TorXakis.

Petra van den Bos, Jan Tretmans

BTestBox: A Tool for Testing B Translators and Coverage of B Models

Abstract

The argument of correctness in refinement-based formal software design often disregards source code analysis and code generation. To mitigate the risk of errors in these phases, certifications issued by regulation entities demand or recommend testing the generated software using a code coverage criteria. We propose improvements for the BTestBox, a tool for automatic generation of tests for software components developed with the B method. BTestBox supports several code coverage criteria and code generators for different languages. The tool uses a constraint solver to produce tests, thus being able to identify dead code and tautological branching conditions. It also generates reports with different metrics and may be used as an extension to the Atelier B. Our tool performs a double task: first, it acts on the B model, by checking the code coverage. Second, the tool performs the translation of lower level B specifications into programming language code, runs tests and compares their results with the expected output of the test cases. The present version of BTestBox uses parallelisation techniques that significantly improve its performance. The results presented here are encouraging, showing performance numbers that are one order of magnitude better than the ones obtained in the tool’s previous version.

Diego de Azevedo Oliveira, Valério Medeiros Jr., David Déharbe, Martin A. Musicante

Predicting and Testing Latencies with Deep Learning: An IoT Case Study

Abstract

The Internet of things (IoT) is spreading into the everyday life of millions of people. However, the quality of the underlying communication technologies is still questionable. In this work, we are analysing the performance of an implementation of MQTT, which is a major communication protocol of the IoT. We perform model-based test-case generation to generate log data for training a neural network. This neural network is applied to predict latencies depending on different features, like the number of active clients. The predictions are integrated into our initial functional model, and we exploit the resulting timed model for statistical model checking. This allows us to answer questions about the expected performance for various usage scenarios. The benefit of our approach is that it enables a convenient extension of a functional model with timing aspects using deep learning. A comparison to our previous work with linear regression shows that deep learning needs less manual effort in data preprocessing and provides significantly better predictions.

Bernhard K. Aichernig, Franz Pernkopf, Richard Schumi, Andreas Wurm

Learning Communicating State Machines

Abstract

We consider the problems of learning and conformance testing of components in a modular system. We assume that each component can be modelled as a Finite State Machine (FSM), the topology of the system is known, but some (or all) component FSMs are unknown and have to be learned by testing the whole system, as it cannot be disassembled. Thus the classical problem of active inference of an automaton in isolation is now further lifted to a system of communicating FSMs of an arbitrary topology. As opposed to the existing work on automata learning, the proposed approach neither needs a Minimally Adequate Teacher, also called the Oracle, nor uses it a conformance tester to approximate equivalence queries. The approach further enhances a SAT solving method suggested by the authors and allows to adaptively test conformance of a system with unknown components assuming that internal communications are observable. The resulting tests are much smaller than the classical universal conformance tests derived from the composite machine of the system.

Alexandre Petrenko, Florent Avellaneda

Repairing Timed Automata Clock Guards through Abstraction and Testing

Abstract

Timed automata (TAs) are a widely used formalism to specify systems having temporal requirements. However, exactly specifying the system may be difficult, as the user may not know the exact clock constraints triggering state transitions. In this work, we assume the user already specified a TA, and (s)he wants to validate it against an oracle that can be queried for acceptance. Under the assumption that the user only wrote wrong guard transitions (i.e., the structure of the TA is correct), the search space for the correct TA can be represented by a Parametric Timed Automaton (PTA), i.e., a TA in which some constants are parametrized. The paper presents a process that (i) abstracts the initial (faulty) TA \( ta_{init} \) in a PTA \( pta \); (ii) generates some test data (i.e., timed traces) from \( pta \); (iii) assesses the correct evaluation of the traces with the oracle; (iv) uses the IMITATOR tool for synthesizing some constraints \(\varphi \) on the parameters of \( pta \); (v) instantiate from \(\varphi \) a TA \( ta_{rep} \) as final repaired model. Experiments show that the approach is successfully able to partially repair the initial design of the user.

Étienne André, Paolo Arcaini, Angelo Gargantini, Marco Radavelli

Proving a Non-blocking Algorithm for Process Renaming with TLA

Abstract

Shared-memory concurrent algorithms are well-known for being difficult to write, ill-adapted to test, and complex to prove. Wait-free concurrent objects are a subclass where a process is never prevented from progressing, whatever the other processes are doing (or not doing). Algorithms in this subclass are often non intuitive and among the most complex to prove. This paper presents the analysis and the proof of a wait-free concurrent algorithm that is used to rename processes. By its adaptive and non-blocking nature, the renaming algorithm resists to test, because of the cost of covering all its states and transitions even with a small input set. Thus, a proof has been conducted in

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-31157-5_10/487239_1_En_10_IEq4_HTML.gif

and verified with TLAPS, the

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-31157-5_10/487239_1_En_10_IEq5_HTML.gif

Proof System. This algorithm is itself based on the assembly of wait-free concurrent objects, the splitters, that separate processes. With just two shared variables and three assignments, a splitter seems a simple object but it is not linearizable. To avoid explicitly in-lining it and dealing with its internal state, the proof of the renaming algorithm relies on replacing the splitter with a sequential specification that is proved correct with TLAPS and verified complete by model-checking on finite instances.

Aurélie Hurault, Philippe Quéinnec

Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties

Abstract

A common way to specify software properties is to associate a contract to each function, allowing the use of various techniques to assess (e.g. to prove or to test) that the implementation is valid with respect to these contracts. However, in practice, high-level properties are not always easily expressible through function contracts. Furthermore, such properties may span across multiple functions, making the specification task tedious, and its assessment difficult and error-prone, especially on large code bases. To address these issues, we propose a new specification mechanism called meta-properties. Meta-properties are enhanced global invariants specified for a set of functions, capable of expressing predicates on values of variables as well as memory related conditions (such as separation) and read or write access constraints. This paper gives a detailed presentation of meta-properties and their support in a dedicated Frama-C plugin MetAcsl, and shows that they are automatically amenable to both deductive verification and testing. This is demonstrated by applying these techniques on two illustrative case studies.

Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall

Property-Based Test Case Generators for Free

Abstract

Property-Based Testing requires the programmer to write suitable generators, i.e., programs that generate (possibly in a random way) input values for which the program under test should be run. However, the process of writing generators is quite a costly, error-prone activity. In the context of Property-Based Testing of Erlang programs, we propose an approach to relieve the programmer from the task of writing generators. Our approach allows the automatic, efficient generation of input test values that satisfy a given specification. In particular, we have considered the case when the input values are data structures satisfying complex constraints. That generation is performed via the symbolic execution of the specification using constraint logic programming.

Emanuele De Angelis, Fabio Fioravanti, Adrián Palacios, Alberto Pettorossi, Maurizio Proietti

Backmatter

Titel: Tests and Proofs
herausgegeben von: Dirk Beyer
Chantal Keller
Verlag: Springer International Publishing
Electronic ISBN: 978-3-030-31157-5
Print ISBN: 978-3-030-31156-8
DOI: https://doi.org/10.1007/978-3-030-31157-5