Formal aspects of component software : 17th International Conference, FACS 2021, Virtual event, October 28-29, 2021, Proceedings

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