Recent Trends in Algebraic Development Techniques
20th International Workshop, WADT 2010, Etelsen, Germany, July 1-4, 2010, Revised Selected Papers
Published on 21. February 2012
X, 303 pages
978-3-642-28412-0 (ISBN)
Description
This book constitutes the thoroughly refereed post-conference proceedings of the 20th International Workshop on Algebraic Development Techniques, WADT 2010, held in July 2010 in Etelsen, Germany.
The 15 revised papers presented were carefully reviewed and selected from 32 presentations. The workshop deals with the following topics: foundations of algebraic specification; other approaches to formal specification including process calculi and models of concurrent, distributed and mobile computing; specification languages, methods, and environments; semantics of conceptual modeling methods and techniques; model-driven development; graph transformations, term rewriting and proof systems; integration of formal specification techniques; formal testing and quality assurance validation, and verification.
More details
Other editions
Additional editions
Till Mossakowski | Hans-Jörg Kreowski
Recent Trends in Algebraic Development Techniques
20th International Workshop, WADT 2010, Etelsen, Germany, July 1-4, 2010, Revised Selected Papers
Book
02/2012
1st Edition
Springer
€53.49
Shipment within 7-9 days
Persons
Content
- Title Page
- Preface
- Organization
- Table of Contents
- Invited Talks
- Building a Modal Interface Theory for Concurrency and Data
- Introduction: Basic Principles of System Design
- Modal Input/Output Automata with Data Constraints and Their Refinement
- Compositionality and Compatibility Results
- Related Work
- Conclusion
- References
- My ADT Shrine
- Opening the Shrine
- Early Treasures
- ADT Roots
- Algebraic Domain Equations
- Drifting Away
- Visits Home
- Closing the Shrine
- References
- Evolving SOA in the Q-ImPrESS Project
- References
- Contributed Papers
- Sharing in the Graph Rewriting Calculus
- Introduction
- The Graph Rewriting Calculus
- A Sharing Strategy for the g-calculus
- Properties of the Sharing Strategy
- Adequacy
- Maximal Sharing
- Conclusions
- References
- A New Strategy for Distributed Compensations with Interruption in Long-Running Transactions
- Introduction
- Background on Parallel Sagas
- New Semantics for Parallel Sagas
- Operational and Logical Account
- Discussion and Related Work
- Conclusion
- References
- Towards a First-Order Deontic Action Logic
- Introduction
- Syntax and Semantics
- An Axiomatic System
- Soundness and Completeness
- Related Logics
- An Example
- Conclusions and Further Remarks
- References
- CASL-MDL, Modelling Dynamic Systems with a Formal Foundation and a UML-Like Notation
- Introduction
- CASL-MDL Models
- Entity Types and Type Diagrams
- Datatypes
- Dynamic Types
- Interaction Properties
- Conclusions and Future Work
- References
- Lambda Expressions in CASL Architectural Specifications
- Introduction
- CASL Architectural Specifications
- Semantics of Generic Unit Expressions
- Adding Dependency Tracking
- Completeness of Extended Static Semantics
- Parametric Architectural Specifications
- An Application: Refinement of Units with Imports
- Conclusions
- References
- A Proof Theoretic Interpretation of Model Theoretic Hiding
- Introduction
- Structured Specifications
- LF and MMT
- LF
- LF+MMT
- Representing Logics in LF
- Hiding in LF and MMT
- LF with Hiding
- LF+MMT with Hiding
- Interpreting ASL in LF+MMT
- Logics
- Specifications
- Adequacy for Specifications
- Adequacy for Refinements
- Related Work
- Conclusion
- References
- Towards Logical Frameworks in the Heterogeneous Tool Set Hets
- Introduction
- Preliminaries
- The Heterogeneous Tool Set
- Proof Theoretic Logical Frameworks
- A Logic Atlas in LF
- The LATIN Metaframework
- Main Definition
- Generalizations
- Logical Frameworks in Hets
- Implementing the LMF in Hets
- LF as a Logical Framework in Hets
- Adding a New Logic in Hets: FOL
- Conclusion and Future Work
- References
- An Institution for Graph Transformation
- Introduction
- Background
- Graphs
- Graph Rewriting
- Institutions
- An Institution for GTS
- Signatures
- Sentences
- Models
- Satisfiability
- Satisfaction Condition
- About the Double-Pullback Approach
- Conclusions
- References
- New Results on Timed Specifications
- Introduction and State of the Art
- Background: Real Time Specifications as Games
- Büchi Objectives
- Solving Büchi Games with SOTFTR
- Combining Safety and Büchi objectives
- Case Study
- Timing Diagram Model
- Separate Driver and Sensor Models
- Summary and Future Work
- References
- Combining Graph Transformation and Algebraic Specification into Model Transformation
- Introduction
- Example: Reduction of $SAT3$ to $INDEP$
- Graph Transformational Rule Bases
- Model Transformation
- Assumptions
- Constrained Models and Their Types
- Actions Combining Rules and Operations
- Application of Actions
- Model Transformation Units
- Semantics
- Example
- Interaction between Graph Transformation and Algebraic Specification
- Termination, Functionality and Correctness
- Termination
- Functionality
- Correctness
- Related Work
- Conclusion
- References
- Towards Bialgebraic Semantics for the Linear Time - Branching Time Spectrum
- Introduction
- Bialgebraic Semantics
- Syntax, Signature, -Algebra
- SOS Rules, Transition System, Coalgebra
- Bialgebraic Semantics
- Limitations of Finality
- The Concept of Quasi-finality
- Towards Quasi-final Semantics
- A Transformation of the SOS Rules
- A Proof Approach
- Application to CSP
- Conclusion and Future Work
- References
- Algebraic Signatures Enriched by Dependency Structure
- Introduction
- Motivation
- Dependency Relation
- Category Rset"3223379 and Its Subcategories
- R-multisets and Dependency Bisimulation
- Limits in Rset"3223379
- Colimits in Rset"3223379
- Algebraic Signatures with Dependent Symbols
- Reconstructing Signatures with Dependent Symbols
- Limits and Colimits in AlgSigDep
- Conclusion
- References
- Compositional Modelling and Reasoning in an Institution for Processes and Data
- Introduction
- Loose Process Semantics
- CSP-CASL Institutions for Different CSP Models
- Signatures
- Sentences
- The Alphabet Construction
- Models and Satisfaction
- Pushouts and Amalgamation
- CSP-CASL with Channels
- Refinement and a Structured Proof Calculus
- Refinement
- Compositional Proof Rules along Structuring
- Compositional Verification of Deadlock Freedom
- Deadlock Freedom in Structured Specifications
- Composing Networks
- Example: Online-Shop
- The Specification in Detail
- Deadlock Analysis
- Conclusion and Future Work
- References
- Proving Properties about Functions on Lists Involving Element Tests
- Introduction
- The Earlier Results on Lists, Rephrased
- Refining the Container-Related Notions
- The Type Class $Eq$
- The Type Class $Ord$
- Conclusion and Future Work
- References
- Test-Case Generation for Maude Functional Modules
- Introduction
- Maude
- Maude Functional Modules
- Term Generation
- Testing Maude Functional Modules
- Black-Box Testing
- White-Box Testing
- Enhancing the Performance
- Implementation
- Concluding Remarks and Ongoing Work
- References
- Author Index
