[Lecture Notes in Computer Science] Formal Aspects of Component Software Volume 12018 (16th International Conference, FACS 2019, Amsterdam, The Netherlands, October 23–25, 2019, Proceedings) ||

This book constitutes the thoroughly revised selected papers from the 16th International Conference on Formal Aspects of Component Software, FACS 2019, held in Amsterdam, The Netherlands, in October 2019. The 9 full papers presented together with 9 full papers and 3 short papers as well as 2 other papers were carefully reviewed and selected from 27 submissions. FACS 2019 is concerned with how formal methods can be used to make component-based and service-oriented software development succeed. Formal methods have provided a foundation for component-based software by successfully addressing challenging issues such as mathematical models for components, composition and adaptation, or rigorous approaches to verification, deployment, testing, and certification. 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 This book constitutes revised selected papers of the 8th International Workshop on Formal Aspects of Component Software, FACS 2011, held in Oslo, Norway in September 2011. The 18 full papers presented together with 3 invited talks were carefully reviewed and selected from 46 submissions. They cover the topics of formal models for software components and their interaction, design and verification methods for software components and services, formal methods and modeling languages for components and services, industrial or experience reports, and case studies, autonomic components and self-managed applications, models for QoS and other extra-functional properties (e.g., trust, compliance, security) of components and services, formal and rigorous approaches to software adaptation and self-adaptive systems, and components for real-time, safety-critical, secure, and/or embedded systems.