Tests and Proofs
5th International Conference, TAP 2011, Zürich, Switzerland, June 30 - July 1, 2011, Proceedings
Published on 28. June 2011
X, 205 pages
978-3-642-21768-5 (ISBN)
Description
This book constitutes the refereed proceedings of the 5th International Conference on Tests and Proofs, TAP 2011, held in Zurich, Switzerland in June/July 2011.
The 12 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 27 submissions. Among the topics covered are model checking, testing systems, test generation, symbolic testing, SAT solvers, SMT solvers, property-based testing, automated test generation, learning-based testing, UML, OCL, specification-based testing, and network testing.
More details
Other editions
Additional editions
Martin Gogolla | Burkhart Wolff
Tests and Proofs
5th International Conference, TAP 2011, Zürich, Switzerland, June 30 - July 1, 2011, Proceedings
Book
06/2011
1st Edition
Springer
€53.49
Shipment within 5-7 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Checking Models, Proving Programs, and Testing Systems
- Introduction
- Some Preliminaries on Entities and Activities in Software Development
- Models and Model-Checking
- Programs and Program Proving
- Systems and Testing Systems
- Using Each other Methods: Cross-Fertilisation
- Using Model-Checkers For Test Generation
- Using Test Methods for Model-Checking
- Using Theorem Provers for Test Generation
- What Is Static, What Is Dynamic?
- Symbolic Executions
- Concolic Testing
- Runtime Verification
- Conclusion
- References
- Tests from Proofs
- Incorporating Coverage Criteria in Bounded Exhaustive Black Box Test Generation of Structural Inputs
- Introduction
- Preliminaries
- The Korat Algorithm
- Incorporating Black Box Coverage to Bounded Exhaustive Search
- Soundness of the Approach
- Case Studies
- Analysing the Assessment of our Case Studies
- Conclusions and Future Work
- References
- Checking the Behavioral Conformance of Web Services with Symbolic Testing and an SMT Solver
- Introduction
- Related Work
- Running Example
- Formal Models for Test Case Generation
- Service Orchestration Model
- Test Purpose Model
- Automatic Test Case Generation
- WS-STSs Product
- Symbolic Execution Tree
- SET Computation
- Tools Support and Experimentations
- Conclusion and Perspectives
- References
- Association of Under-Approximation Techniques for Generating Tests from Models
- Motivations
- Test Generation Process from an Abstraction
- Background
- Model Syntax
- Predicate Abstraction
- Abstraction Formalisation
- Examples
- Electrical System Example
- Simple Illustrative Model
- Abstraction Computation
- Under-Approximation by Existential Concretisation
- Under-Approximation by Universal Concretisation
- Discussion about the Properties of the Algorithm
- Implementation and Experimentations
- Implementation and Optimisation
- Experimental Results
- Related Works
- Conclusion and Further Works
- References
- Security Mutants for Property-Based Testing
- Introduction
- HLPSL Mutation Operators
- Agent Identifier Mutant
- Nonce Mutant
- Mutant-Implementation Error-Correspondence
- Related Work
- Conclusion
- References
- The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging
- Introduction
- TheSANTE Tool on a Running Example
- Step 1: Value Analysis
- Step 2: Program Slicing
- Step 3: Dynamic Analysis
- Conclusion
- References
- Abstraction Based Automated Test Generation from Formal Tabular Requirements Specifications
- Introduction
- Preliminaries
- Abstracting Requirements Specifications
- Experimental Results
- Conclusion and Future Work
- References
- Correct Code Containing Containers
- Introduction
- Formal Containers
- Contracts in Ada 2012
- Ada Standard Containers
- API Modification: Independent Cursors
- API Addition: Parts of Containers
- FormalSemantics
- Syntax of LIsts
- Operational Semantics of Lists
- Vectors, Sets and Maps
- Axiomatization
- Presentation of Why
- Axiomatization of Lists
- Effectiveness
- Vectors, Sets and Maps
- Validation of the Axiomatization
- Coq Implementation and Proof for Lists
- Vectors, Sets and Maps
- Related Work
- Conclusion
- References
- A Random Testing Approach Using Pushdown Automata
- Introduction
- General Overview
- Motivation
- Layout of the Approach
- Related Work
- Formal Background
- Pushdown Automata
- Context-Free Grammars
- Uniform Random Generation of Successful Paths
- NPA to Context Free Grammars
- Random Generation of Successful Traces
- Experimentation
- Running Example
- Experimental Results
- Conclusion
- References
- Incremental Learning-Based Testing for Reactive Systems
- Introduction
- Learning-Based Testing
- Efficient Learning Algorithms
- Mathematical Preliminaries and Notation
- Bit-Sliced Learning of Kripke Structures
- Incremental Learning for Kripke Structures
- Correctness and Termination of the IKL Algorithms
- A Learning-Based Testing Architecture Using IKL
- Correctness and Termination of the LBT Architecture
- Case Studies and Performance Benchmarking
- The Cruise Controller Model
- The Elevator Model
- Conclusions
- References
- Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models
- Introduction
- Preliminaries
- Object Constraint Language
- Bit-Vector Logic
- Satisfiability Problem
- Problem Formulation
- Encoding of OCL Data Types
- Basic Data Types
- Sets
- Further Collection Types
- Operations on Collection Types
- Case Study
- Conclusion
- References
- State Coverage Metrics for Specification-Based Testing with B¨uchi Automata
- Introduction
- Preliminaries
- Kripke Structures, Traces, and Tests
- Generalized Büchi Automata
- State Coverage for Generalized Büchi Automata
- Model-Checking-Based Test Generation
- Testing-Based Property Refinement
- Experiment
- Conclusions
- References
- Lightweight Testing of Communication Networks with e-Motions
- Introduction
- A Running Example
- Modelling the Communication Network Using e-Motions
- Modelling the Structure
- Modelling Behaviour
- e-Motions
- Specifying the Behaviour of the Network
- Adding Observers for System Monitoring
- Simulating and Analysing the Network
- Tests
- Related Work
- Conclusions and Future Work
- References
- Author Index
