Formal Aspects of Component Software: 18th International Conference, FACS 2022, Virtual Event, November 10–11, 2022, Proceedings (Lecture Notes in Computer Science, 13712)

This book constitutes the thoroughly revised selected papers from the 18th International Symposium, FACS 2022, which was held online in November 2022.The 12 full papers and 1 short paper were carefully reviewed and selected from 25 submissions. FACS 2021 is focusing on the areas of component software and formal methods in order to promote a deeper understanding of how formal methods can or should be used to make component-based software development succeed. Preface Organization Contents Modelling and Verification Compositional Simulation of Abstract State Machines for Safety Critical Systems 1 Introduction 2 The Mechanical Ventilator Milano (MVM) Case Study 2.1 Problem Context 2.2 System Behavioral Description 3 Preliminary Concepts on ASMs and ASMETA 3.1 Modeling Example 3.2 The ASMETA (ASM mETAmodeling) Toolset 4 Compositional Simulation of ASM Models 5 Compositional Modeling and Simulation at Work 6 Discussion and Lesson Learned 7 Related Work 8 Conclusion and Future Directions References Specifying Source Code and Signal-based Behaviour of Cyber-Physical System Components 1 Introduction 2 Motivation and Language Design Goals 3 Background 3.1 Traces for Signals Used by HLS ch2Menghi2020 3.2 Traces for Source Code Used by iCFTL ch2DawesRV2021 4 Hybrid Traces 5 SCSLSyntax 5.1 Examples 6 Semantics 6.1 Determining Values of Terms 6.2 A Semantics Function 7 Language Comparison 7.1 Implications for Software Verification and Validation Processes 8 Ongoing Work 9 Conclusion References Formally Characterizing the Effect of Model Transformations on System Properties 1 Introduction 2 Related Work 3 Background 4 Formalized Model Transformations 5 Transformation Characterization 5.1 Merging the ALTL Formula and the -extended LTS L 5.2 Transforming L_ 5.3 Detecting and Removing Non-Accepting Cycles in T(L_) 5.4 Constructing a Characteristic Formula for T(L_)_ 6 A Progress Example 7 Conclusions References Interpretation and Formalization of the Right-of-Way Rules 1 Introduction 2 Formalization of Right-of-Way Rules 2.1 Basic Definitions 2.2 Convergence, Divergence, and Overtake 3 Properties of the Right-of-Way Rules 4 Comparison with Previous Formalization 4.1 Converging 4.2 Head-On or Nearly So 4.3 Overtaking 4.4 Right-of-Way 5 Aspects of the Right-of-Way Rules Formalization 6 Summary and Conclusion References Formal Model In-The-Loop for Secure Industrial Control Networks 1 Introduction 2 Background 3 System Architecture 4 Black Box Model 5 White Box Model 6 Results and Comparisons 7 Related Work 8 Conclusion References Debugging of BPMN Processes Using Coloring Techniques 1 Introduction 2 Background 3 BPMN Coloration 3.1 Overview 3.2 Folding 4 Tool and Experiments 4.1 Tool 4.2 Empirical Study 4.3 Performance Study 5 Related Work 6 Concluding Remarks References WEASY: A Tool for Modelling Optimised BPMN Processes 1 Introduction 2 Models 3 Tool 4 Experiments 5 Case Study 6 Concluding Remarks References Logics and Semantics Embeddings Between State and Action Based Probabilistic Logics 1 Introduction 2 Discrete-Time Markov Chains 3 Modified Embeddings sld and ald 4 State Based Logics 4.1 PCTL 4.2 PCTL* 5 Action Based Logics 5.1 prHML 5.2 APCTL* 5.3 APCTL 6 Embeddings for Probabilistic Logics 6.1 PCTL*APCTL* 6.2 APCTL*PCTL* 6.3 PCTLAPCTL 6.4 APCTLPCTL 7 Related Work 8 Conclusion References Footprint Logic for Object-Oriented Components 1 Introduction 2 The Programming Language 3 The Specification Language 4 The Hoare Logic of Footprints 5 A Comparison Between Related Approaches 5.1 Footprints 5.2 Dynamic Frames 5.3 Separation Logic 6 Discussion 7 Conclusion References Decompositional Branching Bisimulation Minimisation of Monolithic Processes 1 Introduction 2 mCRL2 3 Cleave and Combine 4 Extension to Branching Bisimilarity 5 Minimisation 6 Experimental Results 7 Conclusion References Types and Choreographies Realisability of Branching Pomsets 1 Introduction 2 Preliminaries on Branching Pomsets 3 Realisability 4 Well-formedness 5 Bisimulation Proof 6 Examples 7 Related Work 8 Conclusion References Liquidity Analysis in Resource-Aware Programming 1 Introduction 2 The Stipula Language 3 Semantics 4 The Theory of Liquidity 5 The Algorithm for Liquidity 6 Related Works 7 Conclusions References Open Compliance in Multiparty Sessions 1 Introduction 2 Calculus 3 Type System 4 Open Compliance 5 Concluding Remarks, Related and Future Works References Author Index