Formal Techniques for Distributed Objects, Components, and Systems (Programming and Software Engineering)

✍ Scribed by Kirstin Peters (editor), Tim A. C. Willemse (editor)

• Publisher: Springer
• Year: 2021
• Tongue: English
• Leaves: 253
• Category: Library

✦ Synopsis

This book constitutes the refereed proceedings of the 41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021, held in Valletta, Malta, in June 2021, as part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021.

The 9 regular papers and 4 short papers presented were carefully reviewed and selected from 26 submissions. They cover topics such as: software quality, reliability, availability, and safety; security, privacy, and trust in distributed and/or communicating systems; service-oriented, ubiquitous, and cloud computing systems; component-and model-based design; object technology, modularity, and software adaptation; self-stabilisation and self-healing/organising; and verification, validation, formal analysis, and testing of the above.

Due to the Corona pandemic this event was held virtually.

✦ Table of Contents

Foreword
Preface
Organization
Contents
Full Papers
On Bidirectional Runtime Enforcement
1 Introduction
2 Preliminaries
3 A Bidirectional Enforcement Model
4 Enforcement
5 Synthesising Action Disabling Monitors
6 Conclusions and Related Work
References
A Multi-agent Model for Polarization Under Confirmation Bias in Social Networks
1 Introduction
2 The Model
2.1 Running Example and Simulations
3 Belief and Polarization Convergence
3.1 Polarization at the Limit
3.2 Convergence Under Confirmation Bias in Strongly Connected Influence
4 Conditions for Polarization
5 Comparison to DeGroot's Model
6 Conclusions and Other Related Work
References
A Formalisation of SysML State Machines in mCRL2
1 Introduction
2 An Informal Introduction to UML State Machines
3 Introduction to mCRL2
4 The Operational Semantics of State Machines
4.1 Strategy to Formalisation
4.2 Abstract Action Language
4.3 Representing State Machines in mCRL2
4.4 Step Selection and Execution
4.5 Change Events
4.6 StateMachine Process
5 SysML Specific Communication
6 Creating a Configuration and Model Checking
7 Discussion and Conclusion
References
How Adaptive and Reliable is Your Program?
1 Introduction
2 Background
3 The Model
4 Towards a Metric for Systems
5 Estimating the Evolution Metric
6 Adaptability and Reliability of Programs
7 Concluding Remarks
References
Branching Place Bisimilarity: A Decidable Behavioral Equivalence for Finite Petri Nets with Silent Moves
1 Introduction
2 Basic Definitions
3 Place Bisimilarity
4 Branching Place Bisimilarity
5 Branching Place Bisimilarity is Decidable
6 Conclusion and Future Research
References
Prioritise the Best Variation
1 Introduction
2 Priority GV
3 Relation to Priority CP
3.1 Revisiting Priority CP
3.2 Correspondence Between PGV and PCP
4 Related Work and Discussion
References
Towards Multi-layered Temporal Models:
1 Introduction
1.1 Ubiquity of Complex Systems
1.2 Heterogeneous Modelling
1.3 Handling Vertical and Horizontal Separation over Temporal Constraints
2 Theoretical Ground
2.1 Time, Partial Orders and Time Structures
2.2 Multi-layered Time Structures
2.3 Horizontal Constraints with CCSL
3 An Example of Multi-layered Modelling
3.1 The Deadlock Petrinet
3.2 A Functional View of the System
3.3 Binding the Two Levels of Description
4 Stakes of the Approach
5 A First Generic CCSL Relation of Refinement
5.1 Definition of 1-N Refinement
5.2 1-N Refinement and Coincidence-Based CCSL Relations
5.3 1-N Refinement and Precedence-Based CCSL Relations
6 A Second Specific CCSL Relation of Refinement
6.1 Definition of 1-1 Refinement
6.2 1-1 Refinement and Coincidence-Based CCSL Relations
6.3 1-1 Refinement and Precedence-Based CCSL Relations
7 Additional Relations of Refinement
8 Conclusion
8.1 Assessments
8.2 Perspectives
References
A Case Study on Parametric Verification of Failure Detectors
1 Introduction
2 Preliminaries
3 Cutoffs of the Failure Detector
4 Encoding the Chandra and Toueg Failure Detector
4.1 The System with One Sender and One Receiver
4.2 Encoding the Message Buffer
4.3 Encoding the Relative Speed of Processes
5 Reduce Liveness Properties to Safety Properties
6 Experiments for Small and
6.1 Model Checkers For TLA+: TLC and APALACHE
6.2 FAST
7 Ivy Proofs for Parametric and
8 Conclusion
References
with Leftovers: A Mechanisation in Agda
1 Introduction
2 Syntax
3 Operational Semantics
4 Resource-Aware Type System
4.1 Multiplicities and Capabilities
4.2 Typing Contexts
4.3 Typing with Leftovers
5 Meta-Theory
6 Conclusions, Related and Future Work
References
Short and Journal-First Papers
Supervisory Synthesis of Configurable Behavioural Contracts with Modalities
References
Off-the-Shelf Automated Analysis of Liveness Properties for Just Paths
1 Introduction
2 Label-Based Justness for mCRL2
3 Off-the-Shelf Verification of Liveness
References
Towards a Spatial Model Checker on GPU
1 Introduction and Background
2 Functional Description and Implementation
2.1 Connected Components Labelling in VoxLogicA-GPU
3 Preliminary Evaluation
4 Conclusions and Future Work
References
Formal Verification of HotStuff
1 Introduction
2 View-Instance and Tree Model for Repeated Consensus
3 Simplified HotStuff Algorithm
3.1 Original HotStuff
4 Verification
5 Conclusion
References
Tutorials
Better Late Than Never or: Verifying Asynchronous Components at Runtime
1 Do You Want to Know a Secret
2 A Day in the Life
3 I Want to Tell You
4 What Goes on
5 The Magical Mystery Tour
6 Come Together
7 Tell Me What You See
8 I'm Only Sleeping
9 Here, There and Everywhere
References
Tutorial: Designing Distributed Software in mCRL2
1 Introduction
2 mCRL2 Primer
3 Mutual Exclusion
3.1 A Naive Algorithm for Mutual Exclusion
3.2 Fixing the Naive Algorithm
3.3 Dekker's Algorithm
3.4 Peterson's Mutual Exclusion Algorithm
4 Epilogue
References
Author Index