Recent Trends in Algebraic Development Techniques [[electronic resource] ] : 23rd IFIP WG 1.3 International Workshop, WADT 2016, Gregynog, UK, September 21–24, 2016, Revised Selected Papers / / edited by Phillip James, Markus Roggenbach

• Pubblicazione: Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017
• Edizione: 1st ed. 2017.
• Descrizione fisica: 1 online resource (X, 223 p. 28 illus.)
• Disciplina: 004
• Soggetto topico: Computer science; Machine theory; Software engineering; Compilers (Computer programs); Computer simulation; Mathematical logic; Computer Science Logic and Foundations of Programming; Formal Languages and Automata Theory; Software Engineering; Compilers and Interpreters; Computer Modelling; Mathematical Logic and Foundations
• Persona (resp. second.): JamesPhillip; RoggenbachMarkus
• Note generali: Includes index.
• Nota di contenuto: 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.
• Sommario/riassunto: 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; and multimedia applications and services.
• Titolo autorizzato: Recent Trends in Algebraic Development Techniques
• ISBN: 3-319-72044-9
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 996465762303316
• Lo trovi qui: Univ. di Salerno
• Serie: Theoretical Computer Science and General Issues, . 2512-2029 ; ; 10644