Formal Techniques for Distributed Objects, Components, and Systems : 42nd IFIP WG 6.1 International Conference, FORTE 2022, Held As Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Lucca, Italy, June

This book constitutes the refereed proceedings of the 42nd IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2022, held in Lucca, Italy, in June 2022, as part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022.The 12 regular papers presented were carefully reviewed and selected from 28 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. Foreword Preface Organization 30+ Years of FORTE Research: A Personal Perspective (Abstract of Invited Talk) Contents Monitoring Hyperproperties with Circuits 1 Introduction 2 The Logic 3 The Monitors 3.1 Runtime Costs 4 Conclusion and Future Work A Appendix: Cases for the Proof of Violation Completeness References Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies Using mCRL2 1 Introduction 2 Background on the XACML Policy Language 3 Modeling and Analyzing XACML Policies 3.1 Mapping XACML Policies into mCRL2 3.2 Specifying the Properties of XACML Policies 4 System Behavior in Presence of XACML Policies 5 Related Work 6 Conclusion References The Reversible Temporal Process Language 1 Introduction 2 Informal Overview of TPL and Reversibility 3 Reversible Temporal Process Language 4 Properties 4.1 Idempatience and Properties of 4.2 Relations with TPL and Reversible CCS 5 Reversibility in revTPL 5.1 Revised Semantics 5.2 Independence 5.3 Causal Consistency 6 Conclusions References Branch-Well-Structured Transition Systems and Extensions 1 Introduction 2 Preliminaries 3 Termination and Boundedness 4 Decidability of Coverability 5 Conclusion References Offline and Online Monitoring of Scattered Uncertain Logs Using Uncertain Linear Dynamical Systems 1 Introduction 2 Related Works 3 Preliminaries 4 Monitoring Using Uncertain Linear Dynamical Systems as Bounding Model 4.1 Offline Monitoring 4.2 Online Monitoring 5 Case Studies 5.1 First Benchmark: Anesthesia 5.2 Second Benchmark: Adaptive Cruise Control 5.3 General Observations 6 Conclusion References Co-engineering Safety-Security Using Statistical Model Checking 1 Context and Motivation 2 AFMTs and Informal Semantics 3 Conclusion References Fault-Tolerant Multiparty Session Types 1 Introduction 2 Fault-Tolerance in Distributed Algorithms 3 Fault-Tolerant Types and Processes 4 A Semantics with Failure Patterns 5 Typing Fault-Tolerant Processes 6 The Rotating Coordinator Algorithm 7 Conclusions References Effective Reductions of Mealy Machines 1 Introduction 2 Definitions 3 SAT-Based Minimization of IGMM 3.1 General Approach 3.2 Proposed SAT Encoding 3.3 Adjustment of Prior Optimizations 3.4 Algorithm 4 Bisimulation with Output Assignment 4.1 Reducing Machines with 4.2 Implementing 5 Benchmarks 6 Conclusion References Traits: Correctness-by-Construction for Free 1 Introduction 2 Motivating Example 3 Object-Oriented Trait-Based Language 3.1 Syntax 3.2 Typing Rules 3.3 Flattening Semantics 3.4 Soundness of the Trait-based CbC Process 4 Trait-Based Correctness-by-Construction in Comparison to Classical CbC 5 Proof-of-Concept Implementation 6 Related Work 7 Conclusion References Encodability Criteria for Quantum Based Systems 1 Introduction 2 Quantum Based Systems 3 Process Calculi 3.1 Communicating Quantum Processes 3.2 An Algebra of Quantum Processes 4 Encodings and Quality Criteria 5 Encoding Quantum Based Systems 6 Separating Quantum Based Systems 7 Quality Criteria for Quantum Based Systems 8 Conclusions References LTL Under Reductions with Weaker Conditions Than Stutter Invariance 1 Introduction 2 Definitions 2.1 A ``Shorter than'' Relation for Infinite Words 2.2 Sensitivity of a Language to the Length of Words 2.3 Relationship to Stutter Insensitive Logic 2.4 When Is Visiting Shorter Words Enough? 3 Application to Verification 3.1 Kripke Structure 3.2 Automata Theoretic Verification 3.3 Detection of Language Sensitivity 3.4 Agglomeration of Events Produces Shorter Runs 4 Experimentation 4.1 A Study of Properties 4.2 A Study of Performances 5 Related Work 6 Conclusion References Computing Race Variants in Message-Passing Concurrent Programming with Selective Receives 1 Introduction 2 Message Races and Selective Receives 3 Execution Traces 4 Computing Message Races and Race Variants 5 Discussion and Future Work References Author Index