Formal Aspects of Component Software: 17th International Conference, FACS 2021, Virtual Event, October 28–29, 2021, Proceedings

Description

This book constitutes the thoroughly revised selected papers from the 17th International Symposium, FACS 2021, which was hel virtually in October 2021. The 7 full papers and 1 short contribution were carefully reviewed and selected from 16 submissions and are presented in the volume together with 1 invited paper. FACS 2021 is concerned with how formal methods can be applied to component-based software and system development. The book is subdivided into two blocks: Modelling & Composition and Verification. Chapter "A Linear Parallel Algorithm to Compute Bisimulation and Relational Coarsest Partitions" is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. Preface Organization Parametric and Interval Model Checking: Recent Advances and Applications (Abstract of Invited Paper) Contents Invited Paper Learning Assumptions for Verifying Cryptographic Protocols Compositionally 1 Introduction 2 Background 2.1 Labeled Transition Systems 2.2 Assumption Learning and Alphabet Refinement 3 An Overview of Taglierino 4 The Attacker Model and Its Correctness 5 Protocol Analysis 5.1 Evaluation Setup 5.2 Needham-Schroeder-Lowe 5.3 Denning-Sacco 5.4 Woo-Lam 5.5 Kerberos 5.6 Performance Evaluation Results 6 Related Work 7 Conclusion References Modelling and Composition Component-Based Approach Combining UML and BIP for Rigorous System Design 1 Introduction 2 System Modeling with UML 2.1 Case Study 2.2 Architecture Model 2.3 Behavior Models 3 From UML to BIP 4 System Simulation and Verification 5 Related Work 6 Conclusion References Composable Partial Multiparty Session Types 1 Introduction 2 A Calculus for Processes over Multiparty Sessions 3 Partial Multiparty Session Types 4 Type System 5 Merging Partial Session Types 5.1 Mapping Merging Functions over Session Types 5.2 Merging Communications and Session Types 6 Subject Reduction and Progress 7 Related Work 8 Conclusions References A Canonical Algebra of Open Transition Systems 1 Introduction 1.1 State from Feedback 1.2 The Algebra of Transition Systems 1.3 Stateful and Stateless Components 1.4 Canonicity and Our Original Contribution 1.5 Related Work 1.6 Synopsis 1.7 Conventions 2 Preliminaries: Categories with Feedback 2.1 Categories with Feedback 2.2 Traced Monoidal Categories 2.3 Delay and Feedback 2.4 St(), the Free Category with Feedback 2.5 Examples 3 Span(Graph): An Algebra of Transition Systems 3.1 The Algebra of Span(Graph) 3.2 The Components of Span(Graph) 3.3 Span(Graph) as a Category with Feedback 3.4 Cospan(Graph) as a Category with Feedback 3.5 Syntactical Presentation of Cospan(FinGraph) 4 Conclusions and Further Work References Corinne, a Tool for Choreography Automata 1 Introduction 2 Choreography Automata 3 Corinne 4 Conclusion, Related Work, and Future Work References Verification Specification and Safety Verification of Parametric Hierarchical Distributed Systems 1 Introduction 2 Preliminaries 3 A Term Algebra of Behaviors 4 The Parametric Safety Problem 4.1 Encoding Invariants and Error Configurations 4.2 The Flow of a Behavioral Term 5 Experimental Evaluation 6 Related Work 7 Conclusions and Future Work References A Linear Parallel Algorithm to Compute Bisimulation and Relational Coarsest Partitions 1 Introduction 2 Preliminaries 2.1 The PRAM Model 2.2 Strong Bisimulation 3 Relational Coarsest Partition Problem 3.1 The Sequential Algorithm 3.2 The PRAM Algorithm 3.3 Correctness 3.4 Complexity Analysis 4 Bisimulation Coarsest Refinement Problem 4.1 The PRAM Algorithm 4.2 Complexity and Correctness 5 Experimental Results 5.1 Experimental Comparison 6 Conclusion References Automated Generation of Initial Configurations for Testing Component Systems 1 Introduction 2 Background 3 Component-Based Model 4 Generation of Initial Configurations 4.1 Combinatorial Algorithm 4.2 Initial Configuration Sampling 4.3 Integration into the Online Test Generation Process 5 Experimentation 6 Related Work 7 Conclusion and Future Works References Monitoring Distributed Component-Based Systems 1 Introduction 2 Preliminaries and Notations 3 Distributed CBS 3.1 Semantics 3.2 Traces 4 Efficient Construction of the Computation Lattice 4.1 Computation Lattice 4.2 Intermediate Operations 4.3 Algorithms for Constructing the Computation Lattice 5 Properties of the Constructed Lattice 5.1 Insensitivity to Communication Delay 5.2 Correctness of Lattice Construction 6 Related Work 7 Conclusions References Author Index