الفهرس 
IntroductionOnly 14 pages are availabe for public view
 |  | from | 103 |  |  |
| | | from | 103 | | |
Abstract
In Machine Learning, neural networks are one of the most studied and commonly used techniques. Despite their popularity, they have limited usage in safety and security- related scenarios where network performance assurance is required. Several solutions have recently developed automated reasoning strategies to bridge the gap between neural networks and applications that require formal guarantees regarding their behavior.
This research focuses on the verification of the safety-critical neural networks which should behave based on the training data and its similarities. This research measures how much percentage of the trained neural network is following the safety-critical principle of making decisions based on prior similarities in training. Evaluation equations measure this percentage to show how much confidence should be given to the trained neural network to be used in a safety-critical application like automated driving systems.
This research utilizes two formal approaches which are Satisfiability (SAT) and Binary Decision Diagram (BDD). This research exposes the pros and cons of each approach and compares the results of each one. Moreover, this research utilizes different algorithms in both approaches to provide various techniques for implementation which give the user the freedom to pick the most suitable one for his use case.
The thesis is divided into six chapters, along with the list of figures, the list of tables, the list of abbreviations, the list of symbols and the bibliography as listed below:
Chapter 1
This chapter gives an introduction to the verification of the safety-critical neural network discussed in this work. It starts by explaining the importance of verifying the safety- critical neural network. Then, a description of the motivations behind this work’s proposed solutions is provided. The objectives of this research are also summarized. A discussion is provided for the designs’ challenges of this work and the methodology used in it. Finally, the road map for the thesis showing its organization is presented.
Chapter 2
This chapter provides the needed background for this study. An overview is given for the concepts of neural networks usage as an algorithm from the widely used machine learning algorithms. The concept of safety-critical neural networks used in this work is explained in detail. Additionally, the Binary Decision Diagram formal method with the utilization of Hamming distance, and satisfiability formal method are presented.
Chapter 3
This chapter illustrates the previous related works in the verification of neural networks in general. Moreover, a detailed description of the formal approaches used to verify the safety-critical neural networks. Then, a focused study of the verification of safety- critical neural networks is provided. Runtime verification is the core approach of the proposed solutions in this work which is one of the formal verification methods to verify safety-critical neural networks. Therefore, its previous related works are presented.
Chapter 4
This chapter presents the proposed architecture of the runtime monitor implemented to verify the safety-critical neural networks. It provides an overview of the proposal architectural model. Then, a detailed explanation is provided for the architecture of the two runtime monitor designs which are the BDD-based runtime monitor and the SAT-based runtime monitor. A discussion of the implementation details in terms of the used methods and algorithms with each formal technique is presented. Additionally, a comparison between the two different conversion algorithms in the satisfiability formal approach is provided. The references used for explaining and implementing the used formal verification approaches are also listed. Eventually, this chapter explains the evaluation equations used for performance assessment of the safety-critical neural networks verification.
Chapter 5
This chapter describes the details of the experimental strategy used in this work. It starts by giving the used tools to setup the verification environment to implement and run the two proposed runtime monitor designs. It shows the neural network architecture and its layers which will be verified using the two proposed designs of the runtime monitor. Additionally, a summary of the MNIST usage is explained. Then, it presents the captured results of the evaluation equations for the two proposed designs with a detailed discussion about the performance evaluation results of the evaluation equations and comparing it to prior works. This chapter provides an explanation of what has been achieved through each proposed approach and the strengths of each one.
Chapter 6
This chapter provides a summary of the work done in this study. It concludes the research conducted in this work and illustrates the potential directions that may be pursued for future work. Additionally, the challenges and difficulties are presented.