Logic, Computation and Rigorous Methods
- Length: 369 pages
- Edition: 1
- Language: English
- Publisher: Springer
- Publication Date: 2021-06-04
- ISBN-10: 3030760197
- ISBN-13: 9783030760199
- Sales Rank: #0 (See Top 100 Books)
This Festschrift was published in honor of Egon Börger on the occasion of his 75th birthday.
It acknowledges Prof. Börger’s inspiration as a scientist, author, mentor, and community organizer. Dedicated to a pioneer in the fields of logic and computer science, Egon Börger’s research interests are unusual in scope, from programming languages to hardware architectures, software architectures, control systems, workflow and interaction patterns, business processes, web applications, and concurrent systems.
The 18 invited contributions in this volume are by leading researchers in the areas of software engineering, programming languages, business information systems, and computer science logic.
From Logic and Computation Theory to Rigorous Methods for Software Engineering Tribute to Egon Börger on the Occasion of His 75th Birthday Acknowledgement Reviewers of this Volume Contents Towards Leveraging Domain Knowledge in State-Based Formal Methods 1 Introduction 2 Domain in Requirements Engineering 3 Ontology-Based Modelling of Domain Knowledge 4 The Nose Gear (NG) Velocity System Case Study 4.1 System Description 4.2 The Case of the Travelled Distance Computation 5 Impact on System Engineering 5.1 The Triptych from State-Based Formal Methods Perspective 5.2 Formalising Domain Knowledge 5.3 Illustration on the Nose Gear Case Study 6 Conclusion References Some Observations on Mitotic Sets 1 Introduction 2 Weakly Mitotic Sets 3 Strongly Mitotic Sets 4 Completeness and Mitoticity References Moded and Continuous Abstract State Machines 1 Introduction 2 ASM, Discrete and Continuous 2.1 Discrete Basic ASM Models 2.2 Continuous ASM Models 3 Example: A Bouncing Tennis Ball 4 Formal Semantics 4.1 Semantic Context 4.2 Operational Semantics 4.3 Mode-Pliant and Pliant-Mode Handovers 4.4 Multiple Subsystems 5 The Tennis Ball Revisited 5.1 The Tennis Ball as a Multiple System 6 Continuous ASM Refinement 6.1 The Discrete Case 6.2 The Continuous Case 6.3 Continuous ASM Refinement and Multiple Subsystems 7 Refinement and the Tennis Ball 8 Related Work 9 Conclusions A The RAQUET Rule References Product Optimization in Stepwise Design 1 To My Friend Egon 2 Similarity of Thought in Scaling Stepwise Design 3 SPL Feature Models and Product Spaces 4 Searching SPL Product Spaces 4.1 Prediction Models 4.2 Finding a Near-Optimal is NP-Hard 4.3 Uniform Random Sampling 5 URS Without Enumeration 6 Performance Configuration Space (PCS) Graphs 7 Analysis of Best-of-n-Samples 8 Another Benefit of URS in Product Optimization 9 Choosing a Sample Set Size 10 Given a Limit of n Samples... 10.1 PCS Graphs of Real SPLs 11 Future Work and Next Steps References Semantic Splitting of Conditional Belief Bases 1 Introduction 2 Background: Conditional Logic 3 Syntax Splitting and Semantic Splitting 4 Optimizing Constraint Systems for C-Representations 5 Constraint Splittings 6 Conclusions and Future Work References Communities and Ancestors Associated with Egon Börger and ASM 1 Background 1.1 Personal Appreciation 2 Communities of Practice 3 The Development of ASM 3.1 Publications 4 A Longterm Historical View 4.1 Logicians 4.2 Polymaths: Astronomers, Geometrists, Mathematicians, Philosophers, Physicists, and Theologians 4.3 Philosophers and Mathematicians 4.4 The Origins of Binary Computing 4.5 Further Academic Advisor Relationships 5 Conclusion 6 Postscript References Language and Communication Problems in Formalization: A Natural Language Approach 1 Introduction 2 Sources of Ambiguity in Requirements 2.1 QuARS 3 Steam Boiler and QuARS 4 Solving Communication Mismatch Problems 4.1 Formalising Vagueness and Quantifiers 4.2 Formalising Disjuncion, Weakness and Temporal Ambiguities: CTL 5 Conclusions A Steam Boiler Requirements References ASM Specification and Refinement of a Quantum Algorithm 1 Introduction 2 Quantum Computation 3 Quantum ASMs 4 ASM Specification of Grover's Algorithm 5 Conclusion References Spot the Difference: A Detailed Comparison Between B and Event-B 1 Introduction 1.1 Classical B 1.2 Event-B 1.3 Tool Support 1.4 Outline 2 Types 3 Formula Language for Expressions and Predicates 3.1 Predicates 3.2 Expressions 3.3 Definitions 3.4 General Missing Features 3.5 Future of B 4 Machines and Refinement 4.1 Events, Operations and Substitutions 4.2 Refinement 4.3 Composition and Modularisation 5 Other Formal Methods 5.1 Event-B by Atelier B 5.2 TLA+ 5.3 Alloy 5.4 ASM, Z 6 Discussion and Conclusion References Some Thoughts on Computational Models: From Massive Human Computing to Abstract State Machines, and Beyond 1 Happy Birthday, Egon Börger! 2 The Logical Origins of the AMS Method 3 MHC-Machines 4 Program Schemes and Unbounded Register Machines 5 Computability over Abstract Structures 6 Computable Queries in Databases 7 Logic vs Engineering 8 P vs NP for Query Languages 8.1 CH-Algebras 8.2 BSS-Computations in Unit Cost 8.3 PCH(D) vs NPCH(D) References Analysis of Mobile Networks' Protocols Based on Abstract State Machine 1 Introduction 2 Abstract State Machines 3 MANET and Routing Protocols 3.1 Ad-hoc On-Demand Distance Vector (AODV) 3.2 NACK-Based AODV (N-AODV) 3.3 Black Hole-Free N-AODV (BN-AODV) 4 MOTION 4.1 Development and Behavior 4.2 Defining the Mobility Model 4.3 The Abstract State Machine-Based Models 4.4 Specific Behavior of the Tool 5 Conclusions and Future Work References What is the Natural Abstraction Level of an Algorithm? 1 Introduction 2 What is an Algorithm? 2.1 Algorithm Execution 2.2 Algorithm Description 2.3 Algorithm Semantics 3 Abstract State Machines 4 Executing Algorithms 4.1 Runtime Structure (States) 4.2 Runtime Changes 5 Describing Algorithms 6 Language Semantics 6.1 Structure (Abstract Syntax) 6.2 (Concrete) Syntax 6.3 Semantics 6.4 Summary 7 Conclusion References The ASMETA Approach to Safety Assurance of Software Systems 1 Introduction 2 The ASMETA Approach 2.1 Project Description 2.2 Abstract State Machines: Background Concepts 2.3 Tool-Support for Safety Assurance 3 ASMETA@design-time 3.1 Modeling 3.2 Validation and Verification 4 ASMETA@development time 4.1 Model-Based Test Generation 4.2 Model-Based Code Generation 4.3 Unit Test Generation 4.4 Behavior-Driven Development Scenarios 5 ASMETA@operation time 5.1 Runtime Simulation 5.2 Runtime Monitoring 6 Conclusion and Outlook References Flashix: Modular Verification of a Concurrent and Crash-Safe Flash File System 1 Introduction 2 Methodology 2.1 Components 2.2 Refinement 2.3 Crash Safety 3 The Flashix File System – Overview 4 Crash-Safe VFS Caching 5 Concurrent Garbage Collection 6 Evaluation 7 Related Work 8 Conclusion References Computation on Structures 1 Towards a Theory of Computation on Structures 2 Parallel Algorithms 2.1 The Parallel ASM Thesis 2.2 Parallel Algorithms with Choice 3 The Logic of Non-deterministic ASMs 3.1 Unrestricted Logic 3.2 Capturing Insignificant Choice 4 Complexity Restriction 4.1 Choiceless Polynomial Time 4.2 Insignificant Choice Polynomial Time 5 Concluding Remarks References The Combined Use of the Web Ontology Language (OWL) and Abstract State Machines (ASM) for the Definition of a Specification Language for Business Processes 1 Introduction 2 Modeling in General 2.1 Static View 2.2 Dynamic View 2.3 Modeling Languages 3 The Parallel Activity Specification Schema: PASS 3.1 General Concept of Subject-Orientation 3.2 Formal Description of PASS 3.3 Combination of Structure and Behavior 4 Discussing the Combination 5 Conclusion References Models and Modelling in Computer Science 1 Models Are the Very First Human Instrument 2 The Fourth Dimension of Computer Science: Modelling 3 Myths About Modelling 4 Models - Towards a General Theory 5 Tasks for Next Decades 6 Finally References A Framework for Modeling the Semantics of Synchronous and Asynchronous Procedures with Abstract State Machines 1 Introduction 2 Abstract State Machine 3 Programming Language Semantics 4 Non-recursive and Recursive Procedures 5 Parameter Passing 6 Functions 7 Procedures as Values 8 Asynchronous Procedures 9 Related Work 10 Conclusions References Author Index
Donate to keep this site alive
1. Disable the AdBlock plugin. Otherwise, you may not get any links.
2. Solve the CAPTCHA.
3. Click download link.
4. Lead to download server to download.