Formal Techniques for Distributed Objects, Components, and Systems (Lecture Notes in Computer Science)

✍ Scribed by Marieke Huisman (editor), António Ravara (editor)

• Publisher: Springer
• Year: 2023
• Tongue: English
• Leaves: 233
• Category: Library

✦ Synopsis

This book constitutes the refereed proceedings of the 43rd IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2023, held in Lisbon, Portugal, in June 2023, as part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023.

The 13 regular papers and 3 short papers presented in this book were carefully reviewed and selected from 26 submissions. They cover topics such as: concurrent programming; security; probabilities, time and other resources; and model-based testing and petri nets.

✦ Table of Contents

Foreword
Preface
Organization
Principles of Persistent Programming (Keynote Talk)
Contents
Concurrent Programming
An Experimental Evaluation of Tools for Grading Concurrent Programming Exercises
1 Introduction
2 Scope
3 Dataset
3.1 The Bank dataset
3.2 The BoundedBuffer dataset
3.3 JBench
4 Tools
4.1 Infer
4.2 Java Pathfinder
4.3 RV-Predict
4.4 MultithreadedTC
5 Results
5.1 Infer
5.2 Java Pathfinder
5.3 RV-Predict
6 Discussion
7 Conclusions
References
Towards an Automatic Proof of the Bakery Algorithm
1 Introduction
2 Preliminaries
2.1 Incremental Induction
2.2 IC3PO: IC3 for Proving Protocol Properties
3 Modeling the Bakery Algorithm
4 Proving Mutual Exclusion of the Bakery Algorithm
4.1 Human-Written Invariant
4.2 Machine-Generated Invariant
4.3 Comparison of the Two Invariants
5 Conclusions
References
Certified Compilation of Choreographies with hacc
1 Introduction
2 Choreographies in hacc
3 Code Generation
4 Conclusion
References
2ptImplementing a CTL Model Checker with muG, a Language for Programming Graph Neural Networks
1 Introduction
2 Preliminaries and Notation
3 A Calculus of Graph Neural Networks
4 From G to TensorFlow
5 G in Action: A CTL Model Checker
5.1 Basics of Computation Tree Logic
5.2 Computation Tree Logic in G
5.3 Evaluation
6 Related Work
7 Conclusion
References
Security
Branching Bisimulation Semantics Enables Noninterference Analysis of Reversible Systems
1 Introduction
2 Background Definitions and Results
2.1 Bisimulation Equivalences
2.2 A Process Calculus with High and Low Actions
2.3 Weak-Bisimilarity-Based Information-Flow Security Properties
3 Use Case: DBMS Transactions – Part I
4 Security Properties Based on Branching Bisimilarity
4.1 Preservation and Compositionality
4.2 Taxonomy of Security Properties
5 Noninterference in Reversible Processes
6 Use Case: DBMS Transactions – Part II
7 Conclusions
References
Impact Analysis of Coordinated Cyber-Physical Attacks via Statistical Model Checking: A Case Study
1 Introduction
2 A Coordinated and Refrigerated Multi-engine System
3 An Implementation in Uppaal SMC
4 An SMC-Based Security Analysis
5 Conclusions, Related and Future Work
References
Probabilities, Time and other Resources
Operations on Timed Scenarios
1 Introduction
2 Preliminaries
2.1 Timed Automata
2.2 Timed Scenarios
2.3 Timed Scenarios and Timed Automata
3 Operations on Scenarios and the Synthesis Problem
4 Subsumption, Intersection and Union
5 Conclusions and Related Work
References
4ptOn the Use of Model and Logical Embeddings for Model Checking of Probabilistic Systems-2pt
1 Introduction
2 Preliminaries
3 Model and Logical Embeddings
4 Implementation
5 Case Studies
5.1 Monty Hall TV Show Problem
5.2 Simulating a Dice Using Fair Coins
5.3 Ant on a Grid
5.4 Lost Boarding Pass Problem
5.5 Bounded Re-transmission Protocol (BRP)
6 Conclusion
References
On Bisimilarity for Polyhedral Models and SLCS
1 Introduction
2 Background and Notation
2.1 Simplex, Simplicial Complexes and Polyhedra
2.2 Simplicial Bisimulation and SLCS on Polyhedral Models
2.3 Face-Poset Models and SLCS
3 -Bisimilarity and the Coincidence Result
4 Conclusions and Future Work
References
Model-Based Testing and Petri Nets
4ptWith a Little Help from Your Friends: Semi-cooperative Games via Joker Moves*-2pt
1 Introduction
2 Concurrent Games
3 Joker Games
4 Properties of Joker Games
5 Joker Games with Randomized Strategies
6 Better Help from Your Friends: Multi-objective and Admissible Strategies
7 Experiments
8 Conclusions
References
Efficient Dynamic Model Based Testing
1 Introduction
2 Related Work
3 Theory of Model Based Testing
4 The MBT Algorithm
5 The Greedy Test Case Selection Strategy
6 Benchmarking Results
6.1 Fault Detection Speed
6.2 Applicability on Large Models
7 Conclusion and Future Work
References
Minimal Generating Sets for Semiflows
1 Introduction and Motivations
1.1 Outline
2 Petri Nets and Semiflows
3 Generating Sets and Minimality
3.1 Basic Definitions and Results
3.2 Minimal Supports and Minimal Semiflows
4 Three Decomposition Theorems
4.1 Decomposition over Non-negative Integers
4.2 Decomposition over Semiflows of Minimal Support
5 Canonical Semiflows
5.1 Canonical and Minimal Semiflows
5.2 About the Number of Canonical Semiflows
6 Minimal Generating Sets, Least Generating Sets, and Fundamental Sets
6.1 Coincidence Between Minimal and Least Generating Sets
6.2 About Fundamental Sets
6.3 About Uniqueness
7 Results Summary
8 Reasoning with Invariants, an Example
8.1 Optimizing Sperner's Bound
8.2 A Proof Scheme Using Minimal Semiflows of Minimal Support
8.3 Further Remarks
9 Conclusion
References
Relating Reversible Petri Nets and Reversible Event Structures, Categorically
1 Introduction
2 Reversible Asymmetric Event Structures
3 Nets with Inhibitor Arcs
4 Reversible Asymmetric Causal Nets
4.1 Asymmetric Causal Nets
4.2 Reversible Asymmetric Causal Nets
5 Relating Models
6 Discussion
References
Author Index