Tests and Proofs
6th International Conference, TAP 2012, Prague, Czech Republic, May 31 -- June 1, 2012. Proceedings
Published on 26. May 2012
X, 177 pages
978-3-642-30473-6 (ISBN)
Description
This book constitutes the refereed proceedings of the 6th International Conference on Test and Proofs, TAP 2012, held in Prague, Czech Republic, in May/June 2012, as part of the TOOLS 2012 Federated Conferences. The 9 revised full papers presented together with 2 invited papers, 4 short papers and one tutorial were carefully reviewed and selected from 29 submissions. The papers are devoted to the convergence of tests and proofs for developing novel techniques and application that support engineers in building secure, safe, and reliable systems. Among the topics covered are model-based testing; scenario-based testing; complex data structure generation; and the validation of protocols and libraries.
More details
Other editions
Additional editions
Achim Brucker | Jacques Julliand
Tests and Proofs
6th International Conference, TAP 2012, Prague, Czech Republic, May 31 -- June 1, 2012. Proceedings
Book
05/2012
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Invited Talks
- The Technology and Psychology of Testing Your Code as You Develop It
- Combining Model Checking and Symbolic Execution for Software Testing
- Research Papers
- From Model-Checking to Automated Testing of Security Protocols: Bridging the Gap
- Introduction
- SAML Web-Browser SSO
- Model Checking
- Specification of the Rules of the Honest Agents
- Specification of the Rules of the Intruder
- Specifying the Authentication Property
- Instrumentation
- Instrumentation of the Rules of the Honest Agents
- Instrumentation of the Rules of the Intruder
- Test Case Execution
- Experimental Results
- Related Work
- Conclusions
- References
- Using Coverage Criteria on RepOK to Reduce Bounded-Exhaustive Test Suites
- Introduction
- Preliminaries
- Reducing Bounded-Exhaustive Test Suites
- On the Effectiveness of Reduced Test Suites
- Case Studies
- Related Work
- Conclusions and Further Work
- References
- A First Step in the Design of a Formally Verified Constraint-Based Testing Tool: FocalTest
- Introduction
- A Brief Presentation of Focalize and FocalTest
- From Focalize to FMON
- From FMON to Constraints
- The FMON Language
- The Constraint Language
- Translating FMON Expressions into Constraints
- Soundness and Completeness of the Constraint Generation
- Conclusion
- References
- Testing Library Specifications by Verifying Conformance Tests
- Introduction
- Background
- The Java Modeling Language
- Unit Testing
- Static Verification
- The Formal CTD Process
- Unit Tests as Operational Behavioral Specifications
- Unit Test Specifications
- The Concrete Process
- JUnit
- The Java Compatibility Kit
- Case Studies
- Conclusion
- References
- Incremental Model-Based Testing of Delta-oriented Software Product Lines
- Introduction
- Foundations
- Model-Based Testing
- Regression Testing
- Delta-Oriented SPL Test Modeling
- Delta-Oriented SPL Regression Testing
- Implementation and Evaluation
- Related Work
- Conclusion
- References
- Conformance Relations for Labeled Event Structures
- Introduction
- Labeled Event Structures
- Observing Event Structures
- Single Action Observations
- Partially Ordered Observations
- Conformance Relations for Concurrent Systems
- Conformance Relations for Input/Output Concurrent Systems
- The ioco Relation for the Interleaving Semantics
- The ioco Relation for the Partial Order Semantics: co-ioco
- Conclusion, Discussion and Future Work
- References
- Test Generation from Recursive Tiles Systems
- Introduction and Motivation
- Conformance Testing Theory for IOLTS
- Recursive Tiles Systems and Their Properties
- Off-Line Test Generation forWeighted RTS
- Construction of the Canonical Tester
- Properties of Generated Test Cases
- On-Line Test Generation from RTS
- Test Case Generation
- Properties of the Test Cases Generated On-Line
- Conclusion
- References
- Generation of Test Data Structures Using Constraint Logic Programming
- Introduction
- The Korat Approach
- The CLP-Based Approach
- Red-Black Trees
- Optimizations
- Experimental Evaluation
- Related Work and Conclusions
- References
- Constructive Finite Trace Analysis with Linear Temporal Logic
- Introduction
- Constructive Finite Trace LTL Matching
- Deterministic Matching with Derivatives
- Checking LTL Coverage by Inspecting Proofs
- Related Work and Conclusion
- References
- Short Papers
- Towards Scenario-Based Testing of UML Diagrams
- Introduction
- Preliminaries
- Formulation of the Model Checking Problem
- Related Work
- Discussion and Future Challenges
- References
- Evaluating and Debugging OCL Expressions in UML Models
- Introduction
- Basic Evaluation Browser Concepts by Example
- General Features Available in the Evaluation Browser
- Further Features Available in the Evaluation Browser
- Related Work
- Conclusion
- References
- A Framework for the Specification of Random SAT and QSAT Formulas
- Motivation
- The Architecture of [q]bfGen
- Tool Demo: The Fixed-Shape Model for QBF
- Conclusion and Future Work
- References
- A Lesson on Structural Testing with PathCrawler-online.com
- Introduction
- Teaching Feedback and Discussion
- The Lesson
- Testing without a Precondition (Test Parameters)
- Definition of a Precondition
- Role of an Oracle in Testing
- Using Structural Testing to Detect a Bug
- Limits of Structural Testing
- Testing with a Specification
- Related Work and Conclusion
- References
- Tutorials
- Tutorial on Automated Structural Testing with PathCrawler
- Author Index
