Tests and Proofs

Name: Tests and Proofs | 5th International Conference, TAP 2011, Zürich, Switzerland, June 30 - July 1, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

5th International Conference, TAP 2011, Zürich, Switzerland, June 30 - July 1, 2011, Proceedings

Martin Gogolla Burkhart Wolff(Herausgeber*in)

Springer (Verlag)

Erschienen am 28. Juni 2011

X, 205 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-21768-5 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken