Correct System Design

Name: Correct System Design | Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015, Proceedings
Brand: Springer
Price: 50.28 EUR
Availability: OnlineOnly

Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015, Proceedings

Roland Meyer André Platzer Heike Wehrheim(Herausgeber*in)

Springer (Verlag)

Erschienen am 3. September 2015

XII, 279 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-23506-6 (ISBN)

50,28 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Preface
Organization
Contents
Laudationes
From Program Verification to Time and Space: The Scientific Life of Ernst-Rüdiger Olderog
Ernst-Rüdiger Olderog: A Life for Meaning
References
Warmest Congratulations, Ernst-Rüdiger!
Semantics
Understanding Probabilistic Programs
1 Introduction
2 Probabilistic Programs
3 Semantic Intricacies
4 Expectation Transformer and Operational Semantics
4.1 Weakest Pre--expectation Semantics
4.2 Operational Semantics
4.3 Relating the Two Semantic Views
5 Program Transformations
6 Conclusion
References
Fairness for Infinitary Control
1 Introduction
2 Basic Concepts
2.1 Infinite Control
2.2 Fairness
2.3 Explicit Scheduling
2.4 The Schedulers S1988 and S2010
3 The Scheduler S2015 for Infinitary Fairness
4 Conclusion
References
Evaluation Trees for Proposition Algebra
1 Introduction
2 Evaluation Trees for Free Valuation Congruence
3 Evaluation Trees for Repetition-proof Valuation Congruence
4 Conclusions
References
Process Algebra
On Applicative Similarity, Sequentiality, and Full Abstraction
1 Introduction
2 Programs and Their Operational Semantics
2.1 Operational Semantics
2.2 The Contextual Preorder
3 Applicative Simulation
4 The Simulation Preorder is a Precongruence
4.1 Howe's Method
5 Full Abstraction
5.1 From Tests to Contexts
References
Causality, Behavioural Equivalences, and the Security of Cyberphysical Systems
1 Motivation
2 Four Ways to Exploit Causality
2.1 Modelling
2.2 Verification
2.3 Decidability and Complexity I
2.4 Decidability and Complexity II
3 Equivalences
3.1 Three Causal Equivalences
3.2 Finite-State Results
3.3 A Hierarchy of Causal Processes
3.4 Infinite-State Results
4 Summary and Outlook
References
Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP
1 Introduction
1.1 Structure Preserving Bisimilarity
1.2 Criteria for Choosing This Semantic Equivalence
1.3 Applying the Criteria
1.4 Inevitability
2 CCSP
3 Petri Nets
4 An Operational Petri Net Semantics of CCSP
5 Structure Preserving Bisimulation Equivalence
6 Strong Bisimilarity
7 Compositionality
8 Processes of Nets and Causal Equivalence
9 A Process-Based Characterisation of Sp-bisimilarity
10 Relating Sp-bisimilarity to other Semantic Equivalences
10.1 Place Bisimilarity
10.2 Occurrence Net Equivalence
10.3 Causal Equivalence
10.4 History Preserving bisimilarity
11 Inevitability for Non-reactive Systems
12 History Preserving Bisimilarity does not Respect Inevitability
13 Structure Preserving Bisimilarity Respects Inevitability
14 Inevitability for Reactive Systems
15 Conclusion
References
Logic
Translating Testing Theories for Concurrent Systems
1 Introduction
1.1 Motivation
1.2 Main Contributions and Overview
2 Runtime Verification and Complete, Unsynchronised Hard Realtime Health Monitors
2.1 Definition
2.2 Health Monitor Design for Kripke Structures and LTL Properties
2.3 An LTL Subclass S' for Unsynchronised Health Monitoring
2.4 Health Monitor H for S'
3 Application to Nondeterministic Programs
3.1 Nondeterministic Programs in Normal Form
3.2 Kripke Structure Semantics
3.3 Example: Health Monitor for Nondeterministic Normal Form Program
4 Health Monitors for CSP Simulations
4.1 CSP Processes with Failures Semantics
4.2 Model Map From Failures Models into Kripke Structures
4.3 Sentence Translation Map and Health Monitor for CSP Processes
5 Conclusions
References
No Need Knowing Numerous Neighbours
1 Introduction
2 Multi-lane Spatial Logic with Scope
2.1 The Model
2.2 The Logic: MLSLS
3 Technical Observability and Stable Models
3.1 An Example of Stability Under Sampling
4 Satisfiability of MLSLS
4.1 A QLIRA Representation of a Traffic Snapshot TS
4.2 Translating Well-Scoped MLSLS Formulas to QLIRA
5 Deciding Stability
6 Conclusion
References
Automated Reasoning Building Blocks
1 Introduction
2 Preliminaries
3 Propositional Superposition
4 CDCL -- Conflict Driven Clause Learning
5 Superposition and CDCL
6 Conclusion
References
Analysis
Being and Change: Reasoning About Invariance
1 Introduction
2 Adaptation Rules
3 Reasoning About Invariance
4 Case Study: Quicksort
5 Future Work
References
Toward Compact Abstractions for Processor Pipelines
1 Introduction
2 Background
2.1 Pipelines
2.2 Concrete Semantics of an In-Order Pipeline
2.3 State-of-the-art Pipeline Analysis
3 Are In-Order Pipelines Interesting? Or: What About Timing Anomalies?
4 Compact Abstract Pipeline Domain Based on Minimal Progress
4.1 Abstract Domain
4.2 Transfer Function
4.3 Diverging and Joining Control Flow
4.4 Why Maximal Progress is not so Important
5 Open Problems
6 Summary and Conclusion
References
Synthesis
Bounded Synthesis for Petri Games
1 Introduction
2 Petri Games
3 Bounded Strategies
4 Finding Bounded Strategies
5 Trade-Offs
6 Conclusions
References
Mediator Synthesis in a Component Algebra with Data
1 Introduction
2 Processes
3 Refinement
4 Parallel Composition
5 Quotient
6 Applications to the Synthesis of Mediators
7 Summary and Future Work
References
Safe and Optimal Adaptive Cruise Control
1 Introduction
2 The Problem of Adaptive Cruise Control
3 Stochastic Priced Timed Games
4 Modeling the Adaptive Cruise Control
4.1 System Component
4.2 The Model of Ego and Front
5 Synthesis and Analysis
5.1 No Strategy
5.2 Safe Strategy
5.3 Safe and Fast Strategy
6 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken