Skip to main content

2010 | Buch

Tests and Proofs

4th International Conference, TAP 2010, Málaga, Spain, July 1-2, 2010. Proceedings

herausgegeben von: Gordon Fraser, Angelo Gargantini

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

insite
SUCHEN

Über dieses Buch

This volume contains the proceedings of TAP 2010, the 4th International C- ference on Tests and Proofs held during July 1–2 in M´ alaga, Spain as part of TOOLS Federated Conferences. TAP 2010wasthe fourth event of an ongoingseriesof conferencesdevoted to the convergence of proofs and tests. In the past, proving and testing were seen as very di?erent and even competing techniques. Proving people would say: If correctness is proved, what do we need tests for? Testers, on the other hand, would claim that proving is too limited in applicability and testing is the only truepathtocorrectness. Ofcourse,bothhaveapoint,buttoquoteEdBrinksma from his 2009 keynote at the Dutch Testing Day and Testcom/FATES: “Who would want to ?y in an airplane with software proved correct, but not tested?” Indeed, the true power lies in the combination of both approaches. Today, m- ern test systems rely on techniques deeply rooted in formal proof techniques, and testing techniques make it possible to apply proof techniques where there was no possibility previously. At a time when even mainstream software engineering conferences start f- turing papers with both “testing” and “proving”in their titles, we are clearly on the verge of a new age where testing and proving are not competing but ?nally accepted as complementary techniques. Albeit, we are not quite there yet, and so the TAP conferences aim to provide a forum for researchers working on the converging topics and to raise general awareness of this convergence.

Inhaltsverzeichnis

Frontmatter

Invited Talks

How Tests and Proofs Impede One Another: The Need for Always-On Static and Dynamic Feedback
Abstract
When creating software, developers rely on feedback in the form of both tests and proofs. The tests provide dynamic feedback from executing the software. The proofs provide static, conservative feedback from analyzing the source code. Testing is widely adopted in practice, but type systems are the only variety of proof to achieve widespread adoption.
Dynamic and static feedback provide complementary benefits, and neither one dominates the other. Sometimes, sound global static checking is most useful. At other times, running tests is most useful. Unfortunately, current languages and IDEs impose too rigid a model of the development process. As a result, the developer is not in control of the development process. In situations where a small amount of appropriate feedback could have yielded insight, the developer must choose between either static or dynamic feedback, and warp his or her development style to the limitations of the language. This situation is wrong: the developer should always have access to immediate execution feedback, and should always have access to sound static feedback.
For example, in a typical statically-typed language, a developer is prevented from running the program if any type errors exist, even if they are not germane to the particular test. In a dynamically-typed (or weakly-typed) language, a developer is free to build insight by experimenting, but never gets the assurance of a proof of type correctness.
We need a better approach. A programmer should be able to view and execute a program through the lens of sound static typing. If the compiler issues no type errors, that is a guarantee (a proof) of static type soundness. A programmer should also be able to view and execute the same program through the lens of dynamic typing with no statically-imposed restrictions. The run-time system should suppress static type errors, unless they lead to user-visible failures, or the developer wishes to examine them. Furthermore, the programmer should be able to switch between these two views as often as desired, or to use them both simultaneously.
A typical use case is: a developer starts from an existing statically-typed codebase (or start writing new code), uses both dynamic and static feedback, and finally restores static type-correctness. Because the developer has types in mind and even uses the type system, large variations from statically-typeable idioms are unlikely.
The ability to execute and run code at any moment is useful in many circumstances, including software creation (e.g., prototyping) and software evolution (e.g., representation or interface changes, library replacement, exploratory changes). Approaches such as prototyping in a dynamic language then rewriting with types, or viewing one part of the program as typed and another part as untyped, address only a subset of these scenarios and impose a significant burden on the developer.
I will describe additional background, theory, and practical details. I will also share experience with an implementation, Ductile, that supports the goal of always-on static and dynamic feedback.
Michael D. Ernst
Myths in Software Engineering: From the Other Side
Abstract
An important component of Empirical Software Engineering (ESE) research involves the measurement, observation, analysis and understanding of software engineering in practice. Results analyzed without understanding the contexts in which they were obtained can lead to wrong and potentially harmful interpretation. There exist several myths in software engineering, most of which have been accepted for years as being conventional wisdom without having been questioned. In this talk we will deal briefly with a few popular myths in software engineering ranging from testing and static analysis to distributed development and highlight the importance of context and generalization.
Nachiappan Nagappan

Specifications from Testing

QuickSpec: Guessing Formal Specifications Using Testing
Abstract
We present QuickSpec, a tool that automatically generates algebraic specifications for sets of pure functions. The tool is based on testing, rather than static analysis or theorem proving. The main challenge QuickSpec faces is to keep the number of generated equations to a minimum while maintaining completeness. We demonstrate how QuickSpec can improve one’s understanding of a program module by exploring the laws that are generated using two case studies: a heap library for Haskell and a fixed-point arithmetic library for Erlang.
Koen Claessen, Nicholas Smallbone, John Hughes

Testing Proofs

Testing First-Order Logic Axioms in Program Verification
Abstract
Program verification systems based on automated theorem provers rely on user-provided axioms in order to verify domain-specific properties of code. However, formulating axioms correctly (that is, formalizing properties of an intended mathematical interpretation) is non-trivial in practice, and avoiding or even detecting unsoundness can sometimes be difficult to achieve. Moreover, speculating soundness of axioms based on the output of the provers themselves is not easy since they do not typically give counterexamples. We adopt the idea of model-based testing to aid axiom authors in discovering errors in axiomatizations. To test the validity of axioms, users define a computational model of the axiomatized logic by giving interpretations to the function symbols and constants in a simple declarative programming language. We have developed an axiom testing framework that helps automate model definition and test generation using off-the-shelf tools for meta-programming, property-based random testing, and constraint solving. We have experimented with our tool to test the axioms used in AutoCert, a program verification system that has been applied to verify aerospace flight code using a first-order axiomatization of navigational concepts, and were able to find counterexamples for a number of axioms.
Ki Yung Ahn, Ewen Denney
Proving and Visualizing OCL Invariant Independence by Automatically Generated Test Cases
Abstract
Within model-driven development, class invariants play a central role. An essential property of a collection of invariants is the independence of each single invariant, i.e., the invariant at hand cannot be deduced from the other invariants. The paper explains with three example models the details of an approach for automatically proving and representing invariant independence on the basis of a script constructing large test cases for the underlying model. Analysis of invariant independence is visualized by means of several diagrams like a ‘test configuration and result’ diagram, an ‘invariant dependence detail’ diagram, and an ‘invariant dependence overview’ diagram. The paper also discusses how to build the test case construction script in a systematic way. The test case construction script is written by the model developer, but a general construction frame for the script is outlined.
Martin Gogolla, Lars Hamann, Mirco Kuhlmann
Proof Process Evaluation with Mutation Analysis
Extended Abstract
Abstract
In the context of deductive proof, formal specification (and thus proofs) may only cover a small part of the program behaviours. We discuss the relevance of applying a mutation analysis, proposed to evaluate the quality of a test set, to evaluate if a specification is able to detect predefined types of faults.
Lydie du Bousquet, Michel Lévy

Test Generation Using Proof Techniques

Generating Regression Unit Tests Using a Combination of Verification and Capture & Replay
Abstract
The combination of software verification and testing techniques is increasingly encouraged due to their complementary strengths. Some verification tools have extensions for test case generation. These tests are strong at detecting software faults during the implementation and verification phase, and to further increase the confidence in the final software product. However, tests generated using verification technology alone may lack some of the benefits obtained by using more traditional testing techniques. One such technique is Capture and Replay, whose strengths are the generation of isolated unit tests and regression test oracles.
Hence, the two groups of techniques have complementary strengths, and therefore are ideal candidates for a tool-chain approach proposed in this paper. The first phase produces, for a given system, unit tests with high coverage. However, when using them to test a unit, its environment is tested as well – resulting in a high cost of testing. To solve this problem, the second phase captures the various executions of the program, which are monitored by the output of the first phase. The output of the second phase is a set of unit tests with high code coverage, which uses mock objects to test the units. Another advantage of this approach is the fact that the generated tests can also be used for regression testing.
Christoph Gladisch, Shmuel Tyszberowicz, Bernhard Beckert, Amiram Yehudai
DyGen: Automatic Generation of High-Coverage Tests via Mining Gigabytes of Dynamic Traces
Abstract
Unit tests of object-oriented code exercise particular sequences of method calls. A key problem when automatically generating unit tests that achieve high structural code coverage is the selection of relevant method-call sequences, since the number of potentially relevant sequences explodes with the number of methods. To address this issue, we propose a novel approach, called DyGen, that generates tests via mining dynamic traces recorded during program executions. Typical program executions tend to exercise only happy paths that do not include error-handling code, and thus recorded traces often do not achieve high structural coverage. To increase coverage, DyGen transforms traces into parameterized unit tests (PUTs) and uses dynamic symbolic execution to generate new unit tests for the PUTs that can achieve high structural code coverage. In this paper, we show an application of DyGen by automatically generating regression tests on a given version of software.
Suresh Thummalapenta, Jonathan de Halleux, Nikolai Tillmann, Scott Wadsworth
Combining Static Analysis and Test Generation for C Program Debugging
Abstract
This paper presents our ongoing work on a tool prototype called sante (Static ANalysis and TEsting), implementing a combination of static analysis and structural program testing for detection of run-time errors in C programs. First, a static analysis tool (Frama-C) is called to generate alarms when it cannot ensure the absence of run-time errors. Second, these alarms guide a structural test generation tool (PathCrawler) trying to confirm alarms by activating bugs on some test cases. Our experiments on real-life software show that this combination can outperform the use of each technique independently.
Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand
Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encoding
Abstract
We consider the problem of test generation for Boolean combinational circuits. We use a novel approach based on the idea of treating tests as a proof encoding rather than as a sample of the search space. In our approach, a set of tests is complete for a circuit N, and a property p, if it “encodes” a formal proof that N satisfies p. For a combinational circuit of k inputs, the cardinality of such a complete set of tests may be exponentially smaller than 2 k . In particular, if there is a short resolution proof, then a small complete set of tests also exists. We show how to use the idea of treating tests as a proof encoding to directly generate high-quality tests. We do this by generating tests that encode mandatory fragments of any resolution proof. Preliminary experimental results show the promise of our approach.
Eugene Goldberg, Panagiotis Manolios

Theorem Proving and Testing

Relational Analysis of (Co)inductive Predicates, (Co)algebraic Datatypes, and (Co)recursive Functions
Abstract
This paper presents techniques for applying a finite relational model finder to logical specifications that involve (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions. In contrast to previous work, which focused on algebraic datatypes and restricted occurrences of unbounded quantifiers in formulas, we can handle arbitrary formulas by means of a three-valued Kleene logic. The techniques form the basis of the counterexample generator Nitpick for Isabelle/HOL. As a case study, we consider a coalgebraic lazy list type.
Jasmin Christian Blanchette
Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications
Abstract
We present an approach for verifying dynamic systems specified in rewriting logic, a formal specification language implemented in the Maude system. Our approach is tailored for invariants, i.e., properties that hold on all states reachable from a given class of initial states. The approach consists in encoding invariance properties into inductive properties written in membership equational logic, a sublogic of rewriting logic also implemented in Maude. The invariants can then be verified using an inductive theorem prover available for membership equational logic, possibly in interaction with narrowing-based symbolic analysis tools for rewriting-logic specifications also available in the Maude environment. We show that it is possible, and useful, to automatically test invariants by symbolic analysis before interactively proving them.
Vlad Rusu

Abstraction

Syntactic Abstraction of B Models to Generate Tests
Abstract
In a model-based testing approach as well as for the verification of properties, B models provide an interesting solution. However, for industrial applications, the size of their state space often makes them hard to handle. To reduce the amount of states, an abstraction function can be used, often combining state variable elimination and domain abstractions of the remaining variables. This paper complements previous results, based on domain abstraction for test generation, by adding a preliminary syntactic abstraction phase, based on variable elimination. We define a syntactic transformation that suppresses some variables from a B event model, in addition to a method that chooses relevant variables according to a test purpose. We propose two methods to compute an abstraction A of an initial model M. The first one computes A as a simulation of M, and the second one computes A as a bisimulation of M. The abstraction process produces a finite state system. We apply this abstraction computation to a Model Based Testing process.
Jacques Julliand, Nicolas Stouls, Pierre-christophe Bué, Pierre-Alain Masson
Building a Test-Ready Abstraction of a Behavioral Model Using CLP
Abstract
This paper proposes an approach for automatically generating model-based tests from a symbolic transition system built as an abstraction of a textual model description written using a pre/postcondition formalism. The abstraction gathers into equivalence classes states from which the same set of operation behaviors can be activated, computed using constraint solving techniques. This abstraction is then used to generate model-based tests using an online test generation technique in which the model animation is guided by the exploration of the abstraction. We apply this approach on the B abstract machines formalism, and compare with a commercial tool, named Leirios Test Generator. We show that our approach makes it possible to achieve a wider variety of test cases, by exploiting the knowledge of the model topology, resulting in an improved fault detection capability.
Pierre-Christophe Bué, Frédéric Dadeau, Adrien de Kermadec, Fabrice Bouquet
Backmatter
Metadaten
Titel
Tests and Proofs
herausgegeben von
Gordon Fraser
Angelo Gargantini
Copyright-Jahr
2010
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-13977-2
Print ISBN
978-3-642-13976-5
DOI
https://doi.org/10.1007/978-3-642-13977-2

Premium Partner