Verification and Evaluation of Computer and Communication Systems: 14th International Conference, VECoS 2020, Xi'an, China, October 26–27, 2020, Proceedings

Preface
Organization
Contents
Petri-Net, Simulation, and Scheduling
An Approach for Supervisor Reduction of Discrete-Event Systems
1 Introduction
2 Preliminaries
2.1 Basics of Automata
2.2 Supervisory Control Theory
3 Proposed Approach
3.1 Problem Formalization
3.2 Framework of the Proposed Approach
3.3 Derivation of R from the Supremal Supervisor S
3.4 A Sufficient Condition for Guaranteeing T Isomorphic to S
4 Illustrative Examples
4.1 Example 1
4.2 Example 2
5 Conclusion and Future Work
References
Multi-robot Path Planning Using Petri Nets
1 Introduction
2 Preliminaries
3 Problem Descriptions
4 PN Synthesis Method for Modeling Multi-robot Systems
4.1 PN Model for a Multi-robot System
4.2 Synthesis Method of Control Places Enforcing the Sub-specification b
4.3 Synthesis Method of Observing Places Enforcing the Sub-specification G
4.4 Synthesis Method of Recording Places Enforcing the Sub-specification V and
5 ILP Problem Obtained by PNs
6 Numerical Experiments
7 Conclusion
References
Deadlock Avoidance of Flexible Manufacturing Systems by Colored Resource-Oriented Petri Nets with Novel Colored Capacity
1 Introduction
2 Realization of Control Policies for Interactive Subnets
3 FMS Example
4 Conclusion
References
The Modeling and Simulation on SRM Drive System Using Variable-Proportional-Desaturation PI Regulator
1 Introduction
2 The Overall Design of the SRM Drive System
3 The Optimized Design of Speed Regulator for SRM Drive System
3.1 Integral Saturation of PI Regulator
3.2 The Design of Variable-proportional-desaturation Speed PI Regulator
3.3 VPDPI Regulator Parameter Adjusting
4 The Simulation Analysis and Performace Analysis of SRM Drive System
4.1 The Performance Analysis of the Drive System Under Rated Speed with No-Load
4.2 The Performance Analysis of the Drive System Under Variable Speed and Load Operation
5 Conclusion
References
Vehicle Scheduling Problem in Terminals: A Review
1 Introduction
1.1 Background
1.2 Introduction to Terminal Operations
2 Vehicle Scheduling Problem in Terminal
2.1 Introduction to Vehicle Scheduling Problem in Terminal
2.2 Fleet Sizing Problem
2.3 Vehicle Dispatching Problem
2.4 Path Planning Problem
3 Conclusions and Outlook
References
Coverage Analysis of Net Inscriptions in Coloured Petri Net Models
1 Introduction
2 Coverage Analysis and MC/DC
3 Instrumentation of CPN Models
3.1 MC/DC Coverage for CPN Models
3.2 Instrumentation of Net Inscriptions
4 Post Processing of Coverage Data
5 Evaluation on Example Models
6 Related Work
7 Summary and Outlook
References
ON/OFF Control Trajectory Computation for Steady State Reaching in Batches Petri Nets
1 Introduction
2 Preliminaries
2.1 Generalized Batches Petri Nets
2.2 Controlled GBPN and Steady State
3 Steady Flow Based ON/OFF Control
4 Maximal Flow Based ON/OFF Control
4.1 Proposed Control Strategy
4.2 Computation of the Timed Control Trajectory
4.3 Transient Behavior of the Controlled Net
5 Study Case
6 Conclusions
References
Towards Efficient Partial Order Techniques for Time Petri Nets
1 Introduction
2 Time Petri Nets
2.1 Definition and Semantics
2.2 Contracted State Class Graph
2.3 Interleavings in the CSCG
3 Stubborn Sets Method Without POSETs
3.1 Stubborn Sets of State Classes and Their Limitations
3.2 Revisited Stubborn Sets Without POSETs
4 Conclusion
References
Towards a Generic Framework for Formal Verification and Performance Analysis of Real-Time Scheduling Algorithms
1 Introduction
2 Contribution and Related Work
2.1 Related Work
2.2 Contribution
3 Modeling and Formulation
3.1 Formal Model of the Processors Layer
3.2 Formal Model of the Clusters Layer
4 Instantiation at the Scheduling Layer
5 Formal Verification and Performance Analysis
5.1 Formal Verification
5.2 Performance Analysis
6 Conclusion
References
Accurate Strategy for Mixed Criticality Scheduling
1 Introduction
2 Related Work
3 The Problem Statement
4 Accurate Fault Mode Strategy
5 Feasibility and Schedulability Analysis
5.1 A Timed Game Model
5.2 Exact Feasibility and Schedulability Tests
6 Illustrative Example
6.1 Decrease the Number of Sacrificed LO Criticality Jobs
6.2 LO Criticality Jobs Are Necessary in Some HI Criticality Configurations
7 Conclusion
References
Formal Modeling and Verification, Testing
Model-Based Design of Resilient Systems Using Quantitative Risk Assessment
1 Introduction
2 Related Work
3 A Rigorous Framework for Modeling and Analyzing Stochastic Timed Systems
3.1 Stochastic Real-Time BIP
3.2 The SMC-BIP Engine
4 A Model-Based Approach Integrating Quantitative Risk Assessment
5 Planetary Robotics Case Study
6 Three Steps of the Approach on the Case Study
6.1 On Robustness to Faults
6.2 On System Performance
7 Discussion
References
An Evaluation of Estimation Techniques for Probabilistic Verification
1 Introduction
2 Integral Estimation Methods
3 Confidence Interval Estimation and Error Analysis
3.1 Intervals Based on the Standard CLT Interval
3.2 Alternative Intervals Based on the Beta-Function
4 Results
4.1 Border Probability Cases
4.2 MC and QMC Error Comparison
4.3 Hybrid Systems Results
5 Conclusions
References
Formal Verification of a Certified Policy Language
1 Introduction
2 Rules, Decisions, Queries, and Policies
2.1 Syntax in Coq
2.2 Evaluating Queries Against Policy Rules
2.3 Ordering Relation on Decisions, Queries and Policies
3 Constraints and Predicates
3.1 Syntax in Coq
3.2 Evaluating Queries Against Constraints
3.3 Conditions on Predicates
4 Properties of TEpla and Their Formalization
4.1 Order Preservation of TEpla Queries
4.2 Non-decreasing Property of TEpla Policies
4.3 Independent Composition of TEpla Policies
5 Conclusion
References
Multi-path Coverage of All Final States for Model-Based Testing Theory Using Spark In-memory Design
1 Introduction
2 Background
2.1 Model-Based Testing
2.2 Apache Spark
3 Problem of Coverage
4 Proposed Spark Coverage Technique
4.1 Input Stage: Automaton Partition
4.2 Map Stage: Intermediate States Coverage
4.3 Reduce Stage: Merging All States Coverage
5 Experiment Results
6 Conclusion and Perspectives
References
Artificial Intelligence and Machine Learning
A C-IFGSM Based Adversarial Approach for Deep Learning Based Intrusion Detection
1 Introduction
2 Related Work
3 Background
3.1 IFGSM
3.2 Analysis of NSL-KDD Dataset
4 C-IFGSM Based Adversarial Approach for Deep Learning-Based Intrusion Detection
4.1 Framework
4.2 Deep Learning-Based Intrusion Detection
4.3 Crafting Adversarial Examples for Intrusion Detection
5 Experiment and Evaluation
5.1 Experiment Setup
5.2 Evaluation Measures
5.3 Experiment
5.4 Evaluation and Discussion
6 Conclusion
References
Deep Reinforcement Learning for Solving AGVs Routing Problem
1 Introduction
2 AGVs Routing Problem
2.1 AGVs System
2.2 AGVs Routing
3 DRL Framework
3.1 Reinforcement Learning
3.2 Modeling Routing Problem Based on MDPs
3.3 Use Asynchronous DQN as the Base Framework
3.4 Reward Setting
3.5 Multi-agent Reinforcement Learning
4 Feature Processing
4.1 Discretization of Continuous Features
4.2 One-Hot Code
4.3 Embedding Code
4.4 Comparison of Input Size of One-Hot and Embedding
5 Neural Network Architecture
5.1 Formation of Conflict Vectors
5.2 Conflict Vectors Processing
6 Experiments
6.1 Comparison of One-Hot and Embedding
6.2 Results
7 Conclusion
References
Research on Vehicle Detection Based on Visual Convolution Network Optimization
1 Introduction
2 Optimize the Convolutional Neural Network by Visualization
2.1 Visual Analysis Method
2.2 Optimize the Network with Visualization
3 Analysis of Experimental Results
4 Conclusion
References
A Self-adaptive Multi-hierarchical Modular Neural Network for Complex Problems
1 Introduction
2 The Structure of the BMNN
3 Construction of the BMNN Structure
3.1 Division of the Function Modules
3.2 Division of the Sub-modules in Each Function Module
3.3 Select Sub-modules from Function Modules
3.4 Integration the Output of Sub-modules
3.5 Self-adaptively Construction the Structure of Sub-modules
4 Experiments and Analysis
4.1 Two-Spiral Problem
4.2 The Real Life Data Regression
5 Conclusion
References
Multi-scale Risk Assessment Model of Network Security Based on LSTM
1 Introduction
2 A Single-Scale Risk Assessment Model for Network Security Based on LSTM
2.1 Time Series Anomaly Detection
2.2 Time Series Anomaly Detection Model Based on LSTM
2.3 A Single-Scale Risk Assessment Model
3 Multi-scale Risk Assessment Model of Network Security Based on LSTM
3.1 Wavelet Analysis
3.2 Multi-scale Risk Assessment Model
4 Experiment
4.1 Data Synthesis
4.2 Single Scale Assessment of Network Security Risk
4.3 Multi-Scale Risk Assessment of Network Security
5 Conclusion
References
Weighted Lightweight Image Retrieval Method Based on Linear Regression
1 Introduction
2 Preliminaries
2.1 Image Hash Algorithm
2.2 Color Model Conversion
2.3 Similarity Calculation
3 The Proposed Algorithm
3.1 Similarity Acquisition
3.2 Multivariable Linear Regression Model
4 Experimental Results and Analysis
4.1 Results of Separate Retrieval for Each Algorithm
4.2 Hash and Color Fusion
4.3 Fusion of Hash and Color Moments Obtained by Linear Regression
5 Conclusion
References
Author Index