Formal Aspects of Component Software: 16th International Conference, FACS 2019, Amsterdam, The Netherlands, October 23–25, 2019, Proceedings (Programming and Software Engineering)

Preface
Organization
Contents
Invited Papers
Modeling Guidelines for Component-Based Supervisory Control Synthesis
	1 Introduction
	2 Preliminaries
		2.1 Finite Automata
		2.2 Extended Finite Automata
		2.3 Supervisory Control Theory
	3 Modeling Independent Components
		3.1 Autonomous Robot
		3.2 Waterway Lock
	4 Modeling Physical Relations
	5 Modeling with the Input-Output Perspective
		5.1 Industrial Examples
	6 Conclusion and Future Work
	References
Modelling and Analysing Software in mCRL2
	1 Introduction
	2 A Short Primer in mCRL2
		2.1 Data Types
		2.2 Processes
		2.3 Modal Formulas
	3 Using the mCRL2 Toolset
	4 Peterson\'s Mutual Exclusion Algorithm
	5 Knuth\'s Dancing Links
	6 Concurrent Data Structures
		6.1 Treiber\'s Stack
		6.2 Lamport\'s Queue
	References
Regular Papers
A Formally Verified Model of Web Components
	1 Introduction
	2 Background
		2.1 Isabelle and Higher-Order Logic
		2.2 The Core DOM
	3 Motivating Example: Fancy Tab
	4 Formalizing Shadow Trees
		4.1 Data Model and Basic Accessors
		4.2 Tree Order and DOM Invariants
	5 Web Components
		5.1 A Formal Definition of Web Components
		5.2 Component Safety
		5.3 Component Safety of the DOM Methods
		5.4 Recommendations
	6 Related Work
	7 Conclusion
	References
Minimizing Characterizing Sets
	1 Introduction
		1.1 Motivation and Problem Statement
		1.2 Results
		1.3 Practical Implications of Our Results and Future Directions
		1.4 Summary of the Paper
	2 Preliminaries
	3 Hardness of K-W-set Problem
	4 Algorithm to Construct Minimum W-Sets
	5 Empirical Evaluation
		5.1 FSMs Used in the Experiments, Experiment Settings and Evaluation
		5.2 Evaluation
		5.3 Threats to Validity
	6 Conclusion
	References
A Bond-Graph Metamodel:
	1 Introduction
	2 Related Work on Bond-Graph Language and Tooling
		2.1 Relation to Software-Modeling Languages
		2.2 Bond-Graph Language in Tooling
	3 Methods on Metamodeling
		3.1 Levels of Abstraction
		3.2 Conforming to Higher-Order Knowledge
		3.3 Conforming to Known Meta-Metamodels
	4 Analysis of Bond-Graph Entities
		4.1 Classification of Bond-Graph Vertices
	5 Formalization of the Bond-Graph Metamodel
		5.1 Formal Definition of Entities, Properties and Constraints
		5.2 Formal Definition of Power Variables
		5.3 A Note on Causality
	6 Metamodel Discussion
		6.1 Properties of the Bond-Graph Metamodel
		6.2 Note on Completeness of the Bond-Graph Metamodel
	7 Interfacing Software Components Using Bond-Graph Entities
		7.1 Use-Case Example: Haptic Telemanipulation
	8 Conclusions
	References
Multilabeled Petri Nets
	1 Introduction
	2 Preliminaries
		2.1 Graded Monoids
		2.2 Multisets
	3 Multilabeled Petri Nets
		3.1 Constraint Automata
	4 Composition
		4.1 Composition Algorithm
	5 Abstraction
		5.1 Sequential Compositions
		5.2 Elimination of Silent Traces
		5.3 Abstraction Algorithm
	6 Conclusion
	References
A Service-Oriented Approach for Decomposing and Verifying Hybrid System Models
	1 Introduction
	2 Preliminaries
		2.1 Simulink
		2.2 KeYmaera X and the Differential Dynamic Logic (dL)
		2.3 Simulink to dL Transformation
	3 Related Work
	4 A Service-Oriented Verification Approach for Hybrid System Models
		4.1 Assumptions
		4.2 Hybrid Contracts
		4.3 Service Verification
		4.4 Service-Oriented System Verification
		4.5 Soundness
	5 Evaluation
	6 Conclusion
	References
Compositional Liveness-Preserving Conformance Testing of Timed I/O Automata
	1 Introduction
	2 Timed Input/Output Automata
	3 Timed Input/Output Conformance
	4 Improved Timed Input/Output Conformance
		4.1 Safe vs. Enforced Quiescence
		4.2 Compositionality
		4.3 Symbolic Live Timed Input/Output Conformance Testing
	5 Tool Support
	6 Related Work
	7 Conclusion
	References
RecordFlux: Formal Message Specification and Generation of Verifiable Binary Parsers
	1 Introduction
	2 Related Work
	3 Modeling and Processing Message Formats
		3.1 Example: Ethernet Frame
		3.2 Message Representation
		3.3 Derivation of Validation and Accessor Functions
		3.4 Message Refinement
	4 Implementation
		4.1 Specification Language
		4.2 Code Generation
		4.3 Verification
	5 Case Studies
		5.1 Verified TLS Parser
		5.2 TLS Heartbeat
	6 Conclusion and Outlook
	A  Deep Embedding
	B  Formal Specification of Ethernet Frame
	References
State Identification for Labeled Transition Systems with Inputs and Outputs
	1 Introduction
	2 Preliminaries
	3 Validity and Compatibility
		3.1 Validity
		3.2 Compatibility
	4 Test Cases
	5 Splitting Graphs
		5.1 Splitting Graph Definition
		5.2 Splitting Conditions
		5.3 Splitting Graph Construction
	6 Extracting Test Cases from a Splitting Graph
	7 Experimental Results on a Case Study
	8 Conclusions and Future Work
	References
Combining State- and Event-Based Semantics to Verify Highly Available Programs
	1 Introduction
	2 A Formal Semantics for Highly Available Programs
	3 Single-Invocation Semantics
	4 Soundness of the Reduction
	5 The Repliss Tool
		5.1 Implementation
		5.2 Specification
		5.3 Correctness
	6 Conclusion and Future Work
	References
Short Papers
Reowolf: Synchronous Multi-party Communication over the Internet
	1 Introduction
	2 Background
	3 Comparing Reo and Reowolf
	4 Programming with Connectors
	5 Leveraging Explicit Protocol Descriptions
	References
Modeling and Verifying Dynamic Architectures with FACTum Studio
	1 Introduction
	2 Background
	3 FACTum Studio 2
	4 Specification of Dynamic Architectures
		4.1 Specifying Datatypes
		4.2 Component Types
		4.3 Architecture Specification
	5 Verification Using Model Checking and ITP
		5.1 Verifying Component Types
		5.2 Verifying the Architecture
	6 Related Work
	7 Conclusion and Outlook
	References
Revisiting Trace Equivalences for Markov Automata
	1 Introduction
	2 Preliminaries
	3 Trace Equivalences
	4 Coarser Trace Equivalences
	5 Connections with Other Models
	6 Conclusions
	References
Author Index