Recent Trends in Algebraic Development Techniques
23rd IFIP WG 1.3 International Workshop, WADT 2016, Gregynog, UK, September 21-24, 2016, Revised Selected Papers
Published on 7. December 2017
X, 223 pages
978-3-319-72044-9 (ISBN)
Description
This book constitutes the thoroughly refereed post-conference proceedings of the 23rd IFIP WG 1.3 International Workshop on Algebraic Development Techniques, WADT 2016, held in September 2016 in Gregynog, UK.
The 9 revised papers presented together with two invited talks, one invited paper and two survey papers were carefully reviewed and selected from numerous submissions and focus on 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 areas, broadly falling into three categories: multimedia content analysis; multimedia signal processing and communications; andmultimedia applications and services.
More details
Other editions
Additional editions
Phillip James | Markus Roggenbach
Recent Trends in Algebraic Development Techniques
23rd IFIP WG 1.3 International Workshop, WADT 2016, Gregynog, UK, September 21-24, 2016, Revised Selected Papers
Book
12/2017
Springer
€53.49
Shipment within 10-15 days
Content
- Intro
- Preface
- Organization
- Contents
- Abstracts of Invited Talks
- Advances in Verification of Multi-agent Systems
- References
- The Distributed Ontology, Model and Specification Language - DOL
- References
- Full Papers of Invited Talks
- Theorising Monitoring: Algebraic Models of Web Monitoring in Organisations
- 1 Introduction
- 2 Concepts and Principles of Monitoring and Interventions
- 2.1 The Approach
- 2.2 Conceptual Framework for Monitoring
- 3 Monitoring Behaviour Modelled by Streams
- 3.1 Monitoring Streams
- 3.2 Storage
- 3.3 Interventions for Streams
- 4 Monitoring in Organisations
- 4.1 Why Employee Monitoring?
- 4.2 What Might Be Monitored and How?
- 4.3 Organisational Web Monitoring
- 5 Stream Model of Organisation Monitoring: Context
- 5.1 Organisation: Entities, Identity and Characteristics
- 5.2 Web Examples
- 5.3 Modelling Web Behaviour
- 6 Stream Model of Organisation Monitoring: Observation, Judgement, Monitoring
- 6.1 Web Content Observation
- 6.2 Data Usage Observation
- 6.3 Records
- 6.4 Monitoring
- 7 Stream Model of Organisation Monitoring: Storage
- 7.1 Histories, Thresholds and Queries
- 7.2 Data and Operations for Storage
- 8 Interventions
- 9 Concluding Remarks
- 9.1 The Monitoring Stack
- 9.2 Next Steps
- References
- Survey Papers
- Asymmetric Combination of Logics is Functorial: A Survey
- 1 Introduction
- 1.1 Motivation and Context
- 1.2 Contributions and Roadmap
- 2 Combination of Logics: A Brief Overview
- 3 Asymmetric Combination of Logics (Institutionally)
- 3.1 Institutions
- 3.2 An Institutional Rendering of Asymmetric Combinations of Logics
- 4 Asymmetric Combinations of Logics as Functors
- 4.1 Lifting Comorphisms
- 4.2 Property Preservation (Conservativity and Equivalence)
- 4.3 Natural Transformations
- 5 Conclusions and Future Work
- References
- Algebraic Model Management: A Survey
- 1 Introduction
- 2 Model Management
- 2.1 Schema Mapping
- 2.2 Query Generation
- 2.3 Mapping Inversion
- 2.4 Mapping Composition
- 2.5 Schema Matching
- 2.6 Further References
- 3 Algebraic Model Management
- 3.1 Algebraic Databases
- 3.2 Schema Mapping
- 3.3 Query Generation
- 3.4 Mapping Composition
- 3.5 Mapping Inversion
- 3.6 Schema Matching
- 4 Conclusion
- References
- Regular Papers
- Probability Functions in the Context of Signed Involutive Meadows (Extended Abstract)
- 1 Introduction
- 1.1 A Survey of Design Options for the Inverse of 0
- 1.2 Working with Involutive Ring Based Meadows
- 2 Boolean Algebras and Meadows
- 2.1 Boolean Algebras
- 2.2 Valuated Boolean Algebras and Some Naming Conventions
- 2.3 Events and Signed Meadows
- 3 Signed Meadow Based Probability Calculus
- 3.1 Equational Axioms for a Probability Function
- 3.2 Conditional Probability as a Total Operator: Four Options
- 3.3 Independence of Events
- 4 Logical Aspects of Equations for Probability Functions
- 4.1 Completeness of BA+Md+Sign+PFP
- 4.2 Using Free Boolean Algebras as Event Spaces
- 5 Multi-dimensional Probability Functions
- 5.1 Equational Axioms for a Probability Function Family
- 5.2 Existence of a Universal Probability Function
- 6 Concluding Remarks
- References
- A Calculus of Virtually Timed Ambients
- 1 Introduction
- 2 Virtually Timed Ambients
- 3 Comparing Virtually Timed Ambients
- 4 Related Work
- 5 Concluding Remarks
- References
- An Institution for Event-B
- 1 Introduction and Motivation
- 1.1 Formal Specification of a Traffic-Lights System in Event-B
- 1.2 Related Work: Institutions and Modularisation
- 2 An Institution for Event-B
- 2.1 Defining EVT
- 3 Relating FOPEQ and EVT
- 3.1 Pushouts and Amalgamation
- 4 Modularising Event-B Specifications
- 4.1 Refinement in the EVT Institution
- 4.2 A Modular, Refined Specification
- 5 Conclusion and Future Work
- References
- On the Most Suitable Axiomatization of Signed Integers
- 1 Introduction
- 2 Definitions of N
- 3 Approach 1: Definition of Z Using Set Theory
- 4 Formal Definitions
- 4.1 Syntactic Notations
- 4.2 Semantic Denotations
- 5 Definitions of Z Using Non-free Constructors
- 5.1 Approach 2: NF21 - Two Sorts and One Non-free Constructor
- 5.2 Approach 3: NF13 - One Sort and Three Non-free Constructors
- 5.3 Approach 4: NF31 - Three Sorts and One Non-free Constructor
- 5.4 Approach 5: NF22 - Two Sorts and Two Non-free Constructors
- 6 Definitions of Z Using Free Constructors
- 6.1 Approach 6: F32 - Three Sorts and Two Free Constructors
- 6.2 Approach 7: F23 - Two Sorts and Three Free Constructors
- 6.3 Approach 8: F22 - Two Sorts and Two Free Constructors
- 6.4 Approach 9: F21 - Two Sorts and One Constructor
- 6.5 Approach 10: F13 - One Sort and Three Free Constructors
- 7 Conclusion
- References
- Observational Semantics for Dynamic Logic with Binders
- 1 Introduction
- 2 D"3223379 -Logic: Background and Motivations
- 2.1 Overview on D"3223379
- 2.2 Motivations
- 3 D"3223379 -Logic
- 3.1 Observational Models Category
- 3.2 Observational Satisfaction
- 4 Recovering Modal Invariance for Bisimulation
- 5 Relating Abstractor and Observational Semantics
- 6 Conclusion
- References
- Towards Critical Pair Analysis for the Graph Programming Language GP 2
- 1 Introduction
- 2 Graphs and Graph Programs
- 2.1 Background
- 2.2 Example: Recognition of Series-Parallel Graphs
- 3 Unification of GP 2 List Expressions
- 4 Symbolic Critical Pairs
- 5 Construction and Finiteness of Symbolic Critical Pairs
- 6 Completeness of Symbolic Critical Pairs
- 7 Conclusion and Future Work
- References
- Canonical Selection of Colimits
- 1 Introduction
- 2 Preliminaries
- 2.1 Categories with Symbols
- 2.2 Specification Operators with Colimit Semantics
- 3 Desirable Properties of Colimit Selections
- 3.1 Symbols of a Diagram
- 3.2 Properties of Colimit Selections
- 4 Colimit Selections for Typical Signature Categories
- 4.1 Sets
- 4.2 Product Categories
- 4.3 Split Fibrations
- 5 Categories for Improved Colimit Selection
- 5.1 Named Specifications
- 5.2 Structured Symbol Names
- 6 Conclusion
- References
- Formalizing and Validating the P-Store Replicated Data Store in Maude*
- 1 Introduction
- 2 Preliminaries: Maude
- 3 Atomic Multicast in Maude
- 3.1 Atomic Multicast in Maude: ``User Interface''
- 3.2 Maude Specification of Atomic Multicast
- 4 P-Store
- 4.1 P-Store in Detail
- 5 Formalizing P-Store in Maude
- 5.1 Class Declarations
- 5.2 Local Execution of a Transaction
- 5.3 Certification Phase
- 6 Formal Analysis of P-Store
- 7 Fixing P-Store
- 8 Related Work
- 9 Concluding Remarks
- References
- Generic Hoare Logic for Order-Enriched Effects with Exceptions
- 1 Introduction
- 2 Preliminaries: Monads and Exceptions
- 3 Order-Enrichment and Innocence
- 4 A Computational Metalanguage
- 5 Semantics
- 6 Hoare Calculus
- 7 Conclusion and Further Work
- References
- Author Index
