Software Verification Approaches

Network Function Virtualization (NFV)

In the beginning, we need to know NFV which through the establishment of VNF (Virtualized Network Function) to achieve some network functions on a common server, switches, memory and other hardware devices, making these network functions on a common hardware device run, do not need to configure a new dedicated network elements, can greatly enhance the flexibility of the network deployment, and lower investment costs.

In the process of realization of network functionality through NFV technology, VNF in the form of software running on the hardware, by way of example and to achieve termination VNF allocation and deallocation of resources.

In order to avoid VNF packet forgery in transit and in storage and tampering, increasing the signature files in the software package VNF, the receiving end after receiving the VNF software package by verifying signature files for VNF package for secure authentication to ensure VNF packet during transmission security; in addition, the receiving end before VNF instantiated need for storage VNF package for secure authentication to ensure VNF package in the store security, which increased VNF instantiation delay, reduce the VNF instantiated performance.

Systems-Theoretic Process Analysis (STPA)

STPA is for identifying harmful circumstances which could lead to accidents and generating detailed safety requirements which must be implemented in the design to prevent the occurrence of these unsafe scenarios in the system. STPA is a top-down process and it addresses many types of hazards of components and their interactions like design errors, software flaws and component interaction failures. One of the advantages of STPA is that it can be applied at any stage of the system development process. STPA is performed by four main steps:

  1. Before conducting an STPA analysis, the safety analysts should establish fundamentals of the analysis (e.g. accidents, the associated hazards) and construct the control structure diagram.
  2. For each control action in the control diagram, the safety analysts must identify the potentially unsafe control actions of the system that could lead to a hazardous state. A unsafe control action is a control action that violates system safety constraints.
  3. Use the identified hazardous control actions to create safety requirements and constraints.
  4. Determine how each potentially hazardous control action, identified in step 2., could occur by augmenting the control structure diagram with a process model.

Software Model Checking (SMC)

SMC is an automatic technique based on a verification model which explore all possible software states in a brute-force manner to prove properties of their execution. The model checking process involves the target software to be formally modeled in the input language of a model checker and specifications (properties) to be formalized in a temporal logic. Many safety-critical software systems are being written in ANSI-C. Therefore, there exist a number of software model checker tools which are used to verify code conducted a comparison and evaluation of existing model checking tools for C code. This comparison showed that the SPIN model checker, a general-purpose model checker, uses an efficient algorithm to reduce the state explosion problem.

Safety Analysis Combining STPA and SMC

This method can derive software safety requirements at the system level and to verify them at the code level. This approach is divided into three kinds of activities:

  1. Deriving software safety requirements using STPA;
  2. Formalizing of safety requirements and
  3. Verifying software against its safety requirements at the code level.

The structure is like this:

Software Verification

Fault Tree Analysis (FTA)

FTA is a top-down, deductive failure analysis in which an undesired state of a system is analyzed using Boolean logic to combine a series of lower-level events. The propose is to understand how systems can fail, to identify the best ways to reduce risk or to determine event rates of a safety accident or a particular system level failure.

This method can divide into 5 steps:

  1. Define the undesired event to study;
  2. Obtain an understanding of the system;
  3. Construct the fault tree;
  4. Evaluate the fault tree;
  5. Control the hazards identified.

本文链接: 欢迎转载!

© 2018.02.08 - 2020.06.02 Mengmeng Kuang  保留所有权利!

UV : | PV :

:D 获取中...

Creative Commons License