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)

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