Verification and Evaluation of Computer and Communication Systems: 16th International Conference, VECoS 2023, Marrakech, Morocco, October 18–20, 2023, Proceedings (Lecture Notes in Computer Science)

This book constitutes the refereed proceedings of the 16th International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS 2023, held in Marrakech, Morocco, during October 18–20, 2023. The 12 full papers included in this book were carefully reviewed and selected from 36 submissions. The topics presented covered a range of subjects, including approaches to improving the scalability and efficiency of formal verification and their applications to blockchain, smart contracts and neural networks. Preface Organization Keynote Speakers On Verifying Concurrent Programs under Weakly Consistent Memory Models How to Use Polyhedral Reduction for the Verification of Petri Nets Contents Factorization of the State Space Construction for Cyclic Systems with Data 1 Introduction 1.1 Related Works 2 Specifications, Data Extension and Factorization 2.1 Gain Estimation 3 Reduced State Space 4 Application to a Network of Timed Automata 4.1 Timed Automata 4.2 A Toy Example 4.3 Experiments on a Cyber-Physical System 5 Conclusion References Verified High Performance Computing: The SyDPaCC Approach 1 Introduction 2 Functional Bulk Synchronous Parallelism 3 An Overview of SyDPaCC 4 Verified Parallel Maximum Segment Sum 5 Experiments 6 Related Work 7 Conclusion References A QoE Driven DRL Approach for Network Slicing Based on SFC Orchestration in SDN/NFV Enabled Networks 1 Introduction 2 SDN and NFV for Network Slicing in 5G and Beyond 3 SFC for Network Slicing in 5G and Beyond 3.1 SFC Orchestration Based on QoE 3.2 Formulating QoE with Respect to QoS 4 DRL Implementation via DQN and Dueling DQN 4.1 DQN 4.2 Dueling DQN 5 Performance Evaluation and Simulation Results 5.1 Key Assumptions 5.2 Simulation Results 6 Conclusion References On Language-Based Opacity Verification Problem in Discrete Event Systems Under Orwellian Observation 1 Introduction 2 Preliminaries 2.1 Petri Net 2.2 Labeled Petri Net 2.3 Some Results on Reachability in Petri Nets 3 Verification of Language-Based Opacity 3.1 Language-Based Opacity Description 3.2 An Integer Linear Programming Solution 4 Orwellian Observation 5 Opacity Verification Under Orwellian Observation 6 Conclusion References An Enhanced Interface-Based Probabilistic Compositional Verification Approach 1 Introduction 2 Probabilistic Systems 2.1 Probabilistic Modeling 2.2 Requirements Specification 3 Interface-Based Verification Approach 3.1 Minimization Phase 3.2 The Composition Phase 3.3 The Verification Phase 4 Experimental Results 5 Conclusion A Appendix References A Sound Abstraction Method Towards Efficient Neural Networks Verification 1 Introduction 2 Related Works 3 Background 4 The Proposed Model Reduction Approach 5 Early Experiments 6 Conclusion References Towards Formal Verification of Node RED-Based IoT Applications 1 Introduction 2 Related Work 3 Preliminaries 3.1 Petri Nets 3.2 Labeled Transition Systems 4 Formalization of Node-RED Applications 4.1 Syntax of a Node-RED Application 4.2 Semantics of a Node-RED Application 5 From Node-RED to Petri Nets 5.1 Formalization of a Node-RED Flow 5.2 Semantics Equivalence/Preservation 6 Example of Application 7 Conclusion and Perspectives References Formal Verification of a Post-quantum Signal Protocol with Tamarin 1 Introduction 2 A KEM-Based Signal Protocol 2.1 The PQ-X3DH Protocol 2.2 The KEM-Double-Ratchet Protocol 3 Tamarin Formal Verification 3.1 Security Properties 3.2 Tamarin Formalization 3.3 Formal Verification Results References A Comparative Study of Online Cybersecurity Training Platforms 1 Introduction 2 Related Works 3 Methodology 4 Results and Discussion 4.1 Overview of Selected Cybersecurity Training Platforms 4.2 Overview of Selected Features and Parameters 4.3 Comparison of Selected Cybersecurity Training Platforms 5 Conclusion and Future Works References White-Box Mutation Testing of Smart Contracts: A Quick Review 1 Introduction 2 Background Materials 2.1 Mutation Testing 2.2 Smart Contracts 3 Related Reviews 4 Mutation Testing of Smart Contracts 5 Conclusion References Blockchain-Based Trust Management for IoMT Environment 1 Introduction 2 Related Work 3 Proposed Solution 3.1 Architecture 3.2 Trust Management Model 3.3 Trust Computation 3.4 Blockchain Network 4 Performance Evaluation 5 Conclusion References Command & Control in UAVs Fleets: Coordinating Drones for Ground Missions in Changing Contexts 1 Introduction 2 Command & Control in a Nutshell 2.1 Command & Control (C2) 2.2 C2 Functions and Approaches 2.3 C2 Agility and C2 Approach Manœuver 3 A Metamodel for Control & Command 3.1 Metamodel Description 3.2 C2 Approaches 4 Tackling C2 (Approach) Agility 4.1 C2 Roles 4.2 Event Communication 4.3 C2 Approaches Manœuvering 5 A C2 System Simulator 6 Conclusion References Author Index