CN111224985B - Communication Protocol Credibility Verification Method - Google Patents

Abstract

The invention discloses a method for verifying the credibility of a communication protocol. The requirements specification is verified, and a verification data set is obtained; according to the verification data set, the specification detection is carried out. Through the above method, the requirement specification can be verified by using the formal verification tool, so as to ensure the security and reliability of the data communication of the computing platform system.

Description

Communication Protocol Credibility Verification Method

technical field

The present invention relates to the technical field of communication, in particular to a method for verifying the credibility of a communication protocol.

Background technique

Computing platform systems play an important role in many fields such as industry and life today. In addition to the traditional personal computer field, they also occupy a very important position in emerging technology fields such as smart factories and smart driving. It is worth noting that today's computing platform is no longer a simple operation of a single node. Today's computing nodes are networked and systematic. The computing platform systems form a powerful platform system through data communication, and the computing platform systems are reliable. The data communication is the basis to ensure the safe operation of the entire software, and the communication between computing platform systems is constrained by the platform's communication protocol.

In the communication protocols of traditional computing platform systems, people generally use natural language to describe them. Although natural language has the advantages of being easy to understand and convenient, it also has many fatal shortcomings. Strictness and ambiguity, etc., will cause different people to have completely different understandings of the protocol description, resulting in incorrect communication protocols. In order to achieve the purpose of safe and reliable data transmission, the method of verifying the communication protocol can detect errors and defects to the greatest extent. Communication protocol verification includes informal verification and formal verification. Informal verification often lacks mathematical rigor. It is difficult to guarantee the quality of the verification results due to the nature and scientific nature.

SUMMARY OF THE INVENTION

The embodiments of the present disclosure provide a method for verifying the credibility of a communication protocol. In order to provide a basic understanding of some aspects of the disclosed embodiments, a brief summary is given below. This summary is not intended to be an extensive review, nor is it intended to identify key/critical elements or delineate the scope of protection of these embodiments. Its sole purpose is to present some concepts in a simplified form as a prelude to the detailed description that follows.

In a first aspect, an embodiment of the present disclosure provides a method for verifying the credibility of a communication protocol, including:

The requirement specification that meets the security transmission index is described by the formal language, and the requirement specification described by the formal language is obtained;

Validate the requirements specification described in the formal language through the formal verification tool, and obtain the verification data set;

Based on the validation dataset, canonical detection is performed.

Further, the requirements for safe transmission of indicators include:

System interface requirements, user interface requirements, hardware interface requirements, software interface requirements, and communication interface requirements.

Further, the requirement specification that meets the security transmission index is described by the formal language, and the requirement specification described in the formal language is obtained, including:

Perform lexical analysis, grammatical analysis, and semantic analysis on the requirements specifications that meet the security transmission indicators, and obtain the analysis results;

Through the formal language description analysis result, the requirement specification of formal language description is obtained.

Further, formal verification tools, including:

Process Analysis Toolkit (PAT).

Further, the validation dataset includes:

Correctness Verification Data Set, Completeness Verification Data Set, Consistency Verification Data Set, and Unambiguity Verification Data Set.

Further, according to the validation data set, perform normative detection, including:

Check whether the specification is correct according to the correctness verification data set;

Check whether the specification is complete according to the completeness verification data set;

According to the consistency verification data set, check whether the specification is consistent;

Detects whether the specification is unambiguous based on the unambiguous validation dataset.

In a second aspect, an embodiment of the present disclosure provides a communication protocol credibility verification device, including:

The formal language description module is used to describe the requirement specification of the security transmission index through the formal language description, and obtain the requirement specification of the formal language description;

The formal verification module is used to verify the requirement specification described in the formal language through the formal verification tool, and obtain the verification data set;

The detection module is used to perform normative detection according to the validation data set.

Further, the requirements for safe transmission of indicators include:

System interface requirements, user interface requirements, hardware interface requirements, software interface requirements, and communication interface requirements.

Further, the formal language description module includes:

The analysis unit is used to perform lexical analysis, syntax analysis, and semantic analysis on the requirement specification that meets the security transmission index, and obtain the analysis result;

The formal language description unit is used to describe the analysis result through the formal language, and obtain the requirement specification of the formal language description.

Further, formal verification tools, including:

Process Analysis Toolkit (PAT).

Further, the validation dataset includes:

Correctness Verification Data Set, Completeness Verification Data Set, Consistency Verification Data Set, and Unambiguity Verification Data Set.

Further, the detection module includes:

The correctness detection unit is used to verify the data set according to the correctness to detect whether the specification is correct;

The completeness detection unit is used to verify the completeness of the data set according to the completeness of the detection specification;

The consistency detection unit is used to check whether the specification is consistent according to the consistency verification data set;

An unambiguity detection unit for detecting whether the specification is unambiguous based on the unambiguity validation dataset.

The technical solutions provided by the embodiments of the present disclosure may include the following beneficial effects:

The invention provides a method for verifying the credibility of a communication protocol. The requirement specification that satisfies the security transmission index is described by a formal language, and the requirement specification of the formal language description is obtained. Validation, a validation dataset is obtained, and specification detection is performed according to the validation dataset. Through the above method, formal verification tools can be used to verify the requirement specification, which can quickly provide testers with a method to effectively verify the communication protocol of the computing platform system, and can play an active role in the computing platform system with complex functions and strict requirements. , to ensure the security and reliability of the data communication of the computing platform system.

It is to be understood that both the foregoing general description and the following detailed description are exemplary and explanatory only and are not restrictive of the invention.

Description of drawings

The accompanying drawings, which are incorporated in and constitute a part of this specification, illustrate embodiments consistent with the invention and together with the description serve to explain the principles of the invention.

1 is a schematic flowchart of a method for verifying the credibility of a communication protocol according to an exemplary embodiment;

2 is a schematic flowchart of a method for verifying a requirement specification by a formal verification tool according to an exemplary embodiment;

3 is a schematic flowchart of a method for automatically verifying the properties of a model by using a model checking technology according to an exemplary embodiment;

4 is a schematic structural diagram of an apparatus for verifying the credibility of a communication protocol according to an exemplary embodiment;

Fig. 5 is a schematic structural diagram of a detection module according to an exemplary embodiment.

Detailed ways

In order to understand the features and technical contents of the embodiments of the present disclosure in more detail, the implementation of the embodiments of the present disclosure will be described in detail below with reference to the accompanying drawings, which are for reference only and are not intended to limit the embodiments of the present disclosure. In the following technical description, for the convenience of explanation, numerous details are provided to provide a thorough understanding of the disclosed embodiments. However, one or more embodiments may be practiced without these details. In other instances, well-known structures and devices may be shown simplified in order to simplify the drawings.

Example 1:

1 is a schematic flowchart of a method for verifying the credibility of a communication protocol according to an exemplary embodiment;

In some embodiments, a communication protocol credibility verification method, comprising:

Step S101, describing the requirement specification that satisfies the security transmission index through the formal language description, and obtaining the requirement specification described in the formal language;

In some optional embodiments, the computing platform is no longer a simple operation of a single node. Today's computing nodes are networked and systematic, and the computing platform systems form a powerful platform system through data communication. The computing platform system Reliable data communication between computing platforms is the basis for ensuring the safe operation of the entire software, and the communication between computing platform systems is constrained by the platform's communication protocol. A communication protocol refers to the rules and conventions that two entities must abide by to complete communication or services. The protocol defines the format used by the data unit, the information and meaning that the information unit should contain, the connection method, and the timing of information transmission and reception. The data is transferred smoothly to the determined place. In computer communication, the communication protocol is used to realize the standard between the computer and the network connection. If the network does not have a unified communication protocol, the information transmission between the computers cannot be recognized. The communication protocol refers to the communication rules agreed by the parties in advance. It can be simply understood as the common language used by each computer to communicate with each other, and the communication protocol that must be used when two computers communicate.

For complex computing platform systems, safe and reliable transmission between systems is a must. A complete protocol specification should clearly contain five parts: services, the services that the protocol can provide; settings, the settings for the execution environment of the protocol; vocabulary, the collection of data packets required by the actual protocol; encoding, each of the vocabulary in the vocabulary. Encoding format of each data packet; procedural rules, rules to ensure consistent exchange of datagrams.

Specifically, according to the requirements of data security transmission, formulate requirements specifications that meet the security transmission indicators, wherein the requirements are derived from the communication protocol specifications between computing platform systems, and the requirements are functional requirements, including system interface requirements, user interface requirements, and hardware interface requirements. Requirements, software interface requirements, communication interface requirements, memory requirements, and operational requirements.

Requirement specification to meet secure transmission metrics is described in a formal language. Informal description refers to the use of natural language to describe the specification of our data security transmission requirements. In the communication protocol of traditional computing platform systems, people generally use natural language to describe it. Although natural language is easy to understand, convenient, etc. It has many advantages, but it also has many fatal disadvantages. For example, natural language is not accurate enough, not strict enough, and ambiguous, etc., which will cause different people to have completely different understandings of the protocol description, resulting in incorrect communication protocols. Formal description is more precise and stricter than informal description.

Specifically, when using a formal language to describe the requirement specification, first perform lexical analysis, syntax analysis, and semantic analysis on the requirement specification that meets the security transmission index, and obtain the analysis result. The analysis result is described by the formal language. For a given In the formal description language, we choose the appropriate semantic abstract function, and establish the relationship between the formal description and the described object in the equivalence class. This relationship defines an aspect of the description object. In practical applications, by using different semantics Abstract function, we can divide the described object into multiple equivalence classes, make each equivalence class establish an abstract relationship with different formal description languages, and integrate multiple formal description languages into the same semantic domain, so that we can It can describe and analyze many different aspects of the system more comprehensively, and obtain the requirement specification described by formal language.

In the formal description step, the requirements are formally modeled and described using a formal language. When modeling the protocol, we can assign a model to each type of node, and use the process algebraic description language to describe the communication between these process models. By initializing the scheduling request of the asynchronous frame message and modeling the scheduling algorithm in the protocol, the simulation of the scheduling frame information in the protocol cycle is completed. The entire protocol model is composed of the concurrency of the processes of these different types of nodes.

Through the above method, a requirement specification described in a formal language is obtained, and the requirement specification between data communication protocols can be described more precisely and concretely.

Step S102, verifying the requirement specification described in the formal language by a formal verification tool to obtain a verification data set;

Usually, communication protocol verification includes informal verification and formal verification. Informal verification often lacks mathematical rigor and scientificity, and it is difficult to ensure the quality of verification results. Formal verification can be used to discover communication through mathematical analysis. The agreement description is inconsistent, unclear or incomplete. Among them, the formal verification tool is PAT (processanalysis toolkit, process analysis toolkit).

Specifically, after formal modeling of the basic elements of the communication protocol, network operation mechanism, etc., using a formal modeling language, certain rule reasoning or spatial search are used to analyze them rigorously and comprehensively.

2 is a schematic flowchart of a method for verifying a requirement specification by a formal verification tool according to an exemplary embodiment;

In the embodiment of the present disclosure, the specific formal verification steps are shown in FIG. 2 , S201 simulates the communication protocol according to the model simulator, S202 builds a model checking algorithm library, and the model checking algorithm library includes all types of protocol models. Verification algorithms, such as different model checking algorithms for probabilistic models, time models, etc. S203 automatically verifies the properties of the model through model checking technology. The formal verification step mainly relies on model checking techniques. Model checking technology is an automatic verification technology for concurrent systems. The system is represented by a finite state structure, and the properties to be verified can be described by a variety of logics, such as temporal logic. The verification process searches the state space involved. Process that determines the reachability or unreachability of the verified property in the state space.

3 is a schematic flowchart of a method for automatically verifying the properties of a model by using a model checking technology according to an exemplary embodiment;

As shown in Figure 3, when using model checking technology to verify the properties of the model, it includes static analysis and dynamic analysis of the constructed communication protocol model, and dynamic analysis includes logic proof, reachability analysis, and simulation. Proofs include invariance proofs and equivalence proofs, and reachability analysis includes global verification and local verification.

Through the above method, a validation dataset can be obtained.

Step S103 , performing specification detection according to the verification data set.

The specification detection is carried out after the verification of the communication protocol. After verifying the credibility of the communication protocol of the computing platform system, we obtain the verification data set of the communication protocol, and then analyze the correctness, completeness and consistency of the protocol respectively. And four aspects of unambiguity are used to detect the safe transmission of data between systems.

Among them, according to the correctness verification data set, check whether the specification is correct, mainly to check whether each requirement in the correctness verification data set is a requirement that the software should meet, and when each requirement is a requirement that the software should meet, then the The validation dataset is correct, otherwise, the validation dataset is not correct.

According to the completeness verification data set, check whether the specification is complete, mainly check whether the requirements in the completeness verification data set include all important requirements, the definition of software response, the comprehensive marking and indexing of all diagrams, when all the above requirements, definitions, markings and indexes are included. When indexing, the validation data set is complete, otherwise, the validation data set is not complete.

According to the consistency verification data set, check whether the specifications are consistent, mainly to check whether the requirements in the consistency verification data set are internally consistent, when the requirements are internally consistent, the verification data set is consistent, otherwise, the verification data set does not have consistency .

According to the unambiguous verification data set, check whether the specification is unambiguous, mainly to check whether each requirement in the unambiguous verification data set has only one interpretation, when each requirement has only one interpretation, then the verification data The set is unambiguous, otherwise, the validation dataset is not unambiguous.

With the above method, canonical detection can be performed on the validation dataset.

Further, the requirements for safe transmission of indicators include:

System interface requirements, user interface requirements, hardware interface requirements, software interface requirements, and communication interface requirements.

Specifically, according to the requirements of data security transmission, formulate requirements specifications that meet the security transmission indicators, wherein the requirements are derived from the communication protocol specifications between computing platform systems, and the requirements are functional requirements, including system interface requirements, user interface requirements, and hardware interface requirements. Requirements, software interface requirements, communication interface requirements, memory requirements, and operational requirements.

Further, the requirement specification that meets the security transmission index is described by the formal language, and the requirement specification described in the formal language is obtained, including:

Perform lexical analysis, grammatical analysis, and semantic analysis on the requirements specifications that meet the security transmission indicators, and obtain the analysis results;

Through the formal language description analysis result, the requirement specification of formal language description is obtained.

Specifically, when using a formal language to describe the requirement specification, first perform lexical analysis, syntax analysis, and semantic analysis on the requirement specification that meets the security transmission index, and obtain the analysis result. The analysis result is described by the formal language. For a given In the formal description language, we choose the appropriate semantic abstract function, and establish the relationship between the formal description and the described object in the equivalence class. This relationship defines an aspect of the description object. In practical applications, by using different semantics Abstract function, we can divide the described object into multiple equivalence classes, make each equivalence class establish an abstract relationship with different formal description languages, and integrate multiple formal description languages into the same semantic domain, so that we can It can describe and analyze many different aspects of the system more comprehensively, and obtain the requirement specification described by formal language.

In the formal description step, the requirements are formally modeled and described using a formal language. When modeling the protocol, we can assign a model to each type of node, and use the process algebraic description language to describe the communication between these process models. By initializing the scheduling request of the asynchronous frame message and modeling the scheduling algorithm in the protocol, the simulation of the scheduling frame information in the protocol cycle is completed. The entire protocol model is composed of the concurrency of processes of these different types of nodes.

Through the above method, a requirement specification described in a formal language is obtained, and the requirement specification between data communication protocols can be described more precisely and concretely.

Further, formal verification tools, including:

Process Analysis Toolkit (PAT).

Further, the validation dataset includes:

Correctness Verification Data Set, Completeness Verification Data Set, Consistency Verification Data Set, and Unambiguity Verification Data Set.

Further, according to the validation data set, perform normative detection, including:

Check whether the specification is correct according to the correctness verification data set;

Check whether the specification is complete according to the completeness verification data set;

According to the consistency verification data set, check whether the specification is consistent;

Detects whether the specification is unambiguous based on the unambiguous validation dataset.

The specification detection is carried out after the verification of the communication protocol. After verifying the credibility of the communication protocol of the computing platform system, we obtain the verification data set of the communication protocol, and then analyze the correctness, completeness and consistency of the protocol respectively. And four aspects of unambiguity are used to detect the safe transmission of data between systems.

Among them, according to the correctness verification data set, check whether the specification is correct, mainly to check whether each requirement in the correctness verification data set is a requirement that the software should meet, and when each requirement is a requirement that the software should meet, then the The validation dataset is correct, otherwise, the validation dataset is not correct.

According to the completeness verification data set, check whether the specification is complete, mainly check whether the requirements in the completeness verification data set include all important requirements, the definition of software response, the comprehensive marking and indexing of all diagrams, when all the above requirements, definitions, markings and indexes are included. When indexing, the validation data set is complete, otherwise, the validation data set is not complete.

According to the consistency verification data set, check whether the specifications are consistent, mainly to check whether the requirements in the consistency verification data set are internally consistent, when the requirements are internally consistent, the verification data set is consistent, otherwise, the verification data set does not have consistency .

According to the unambiguous verification data set, check whether the specification is unambiguous, mainly to check whether each requirement in the unambiguous verification data set has only one interpretation, when each requirement has only one interpretation, then the verification data The set is unambiguous, otherwise, the validation dataset is not unambiguous.

With the above method, canonical detection can be performed on the validation dataset.

Embodiment 2:

In a preferred embodiment, the trusted verification method of the communication protocol based on the computing platform system of the present invention is used to perform trusted verification on the Powerlink protocol between computing platforms.

The open source real-time communication technology Powerlink is a real-time Ethernet protocol used to solve the real-time data transmission in the field of industrial control and data acquisition on the standard Ethernet medium. The protocol mainly specifies the communication on the data link layer. Communication and aperiodic communication. One protocol cycle mainly includes the isochronous phase and the asynchronous communication phase. The periodic communication occurs in the isochronous phase, and the aperiodic communication occurs in the asynchronous communication phase. Powerlink contains two types of communication nodes. The station node and the slave node, and according to the different communication mechanism between the slave and the master node in the isochronous phase, the slave is divided into three types of nodes, Normal node, PRC node and multiplexing node. In addition, there are five types of frame information in this protocol, and there is scheduling of frame message sending requests in the asynchronous process. In the process of applying the trusted verification method of the communication protocol based on the computing platform system of the present invention to carry out the trusted verification to the Powerlink protocol:

First, it is necessary to obtain the specification of the protocol execution and the security requirements of the data transmission that the protocol needs to meet, so as to facilitate the modeling of the protocol later. The properties that need to be satisfied in the Powerlink protocol include no deadlock, no task "starvation" waiting, real-time and so on.

Then, in the formal description step, the requirements are formally modeled and described using a formal language. When modeling the protocol, we can assign a model to each type of node, and use the process algebraic description language to describe the communication between these process models. By initializing the scheduling request of the asynchronous frame message and modeling the scheduling algorithm in the protocol, the simulation of the scheduling frame information in the protocol cycle is completed. The entire protocol model consists of the concurrency of processes of these different types of nodes. Model the protocol requirements, and describe the protocol's deadlock-free, task-free "starvation" waiting, and real-time characteristics through temporal logic and computational tree logic.

Second, start verifying the protocol. An important function of the formal verification step is to verify the properties satisfied by the protocol according to the protocol model and the formal representation of the protocol requirements. The simulation process can represent all possible paths and state spaces of model execution. Each state can provide hints about the current values of all variables in that state, and transitions between states hint at actions that take place during the operation of the user protocol. Users can debug and analyze the modeling code by simulating different processes. If a deadlock occurs, the location of the deadlock and the reason for the deadlock can also be observed intuitively in the simulation results.

Finally, the verification results are output to the requirements specification evaluation step for processing. For the Powerlink protocol, you can verify whether there is a deadlock in the protocol, whether there are scheduling requests that have not been scheduled, and whether the order of scheduling requests satisfies the priority setting, etc. to evaluate the correctness, completeness, and consistency of the requirements specification. and unambiguous.

Embodiment three:

An embodiment of the present disclosure provides a communication protocol credibility verification apparatus, and FIG. 4 is a schematic structural diagram of a communication protocol credibility verification apparatus according to an exemplary embodiment.

As shown in Figure 4, a communication protocol credibility verification device, comprising:

S401 Formal language description module, which is used to describe the requirement specification of the security transmission index through formal language description, and obtain the requirement specification of formal language description;

S402 a formal verification module, used for verifying the requirement specification described in the formal language through a formal verification tool to obtain a verification data set;

S403, a detection module, configured to perform specification detection according to the verification data set.

Further, the requirements for safe transmission of indicators include:

System interface requirements, user interface requirements, hardware interface requirements, software interface requirements, and communication interface requirements.

Further, the formal language description module includes:

an analysis unit, configured to perform lexical analysis, syntax analysis, and semantic analysis on the requirement specification that meets the security transmission index, and obtain an analysis result;

The formal language description unit is used to describe the analysis result through the formal language to obtain the requirement specification described by the formal language.

Further, the formal verification tool includes:

Process Analysis Toolkit (PAT).

Further, the verification data set includes:

Correctness Verification Data Set, Completeness Verification Data Set, Consistency Verification Data Set, and Unambiguity Verification Data Set.

Further, the detection module includes:

S403-1 Correctness detection unit, used to verify the data set according to the correctness, and detect whether the specification is correct;

S403-2 Completeness detection unit, which is used to verify the completeness of the data set according to the completeness of the detection specification;

S403-3 Consistency detection unit, which is used to verify whether the specifications are consistent according to the consistency verification data set;

S403-4 The unambiguous detection unit is used to detect whether the specification is unambiguous according to the unambiguity verification data set.

A communication protocol credibility verification apparatus provided by an embodiment of the present disclosure executes the communication protocol credibility verification method provided by the above-mentioned embodiments, and will not be described in detail here.

It should be noted:

The algorithms and displays provided herein are not inherently related to any particular computer, virtual appliance, or other device. Various general-purpose devices can also be used with the teachings based on this. The structure required to construct such a device is apparent from the above description. Furthermore, the present invention is not directed to any particular programming language. It should be understood that various programming languages may be used to implement the inventions described herein, and that the descriptions of specific languages above are intended to disclose the best mode for carrying out the invention.

In the description provided herein, numerous specific details are set forth. It will be understood, however, that embodiments of the invention may be practiced without these specific details. In some instances, well-known systems, structures and techniques have not been shown in detail in order not to obscure an understanding of this description.

Similarly, it is to be understood that, in the above description of exemplary embodiments of the invention, various features of the invention are sometimes grouped together into a single embodiment in order to simplify the disclosure and to aid in the understanding of one or more of the various inventive aspects. , figures, or descriptions thereof. However, this disclosed system should not be construed to reflect the intention that the invention as claimed requires more features than are expressly recited in each claim. Rather, as the following claims reflect, inventive aspects lie in less than all features of a single foregoing disclosed embodiment. Thus, the claims following the Detailed Description are hereby expressly incorporated into this Detailed Description, with each claim standing on its own as a separate embodiment of this invention.

Those skilled in the art will appreciate that the steps in the devices in an embodiment can be adaptively changed and placed in one or more devices different from the embodiment. The steps or steps or components in the embodiments may be combined into one step or step or component, and further they may be divided into multiple steps or sub-steps or sub-components. All features disclosed in this specification (including accompanying claims, abstract and drawings) and any system so disclosed may be employed in any combination, unless at least some of such features and/or processes or steps are mutually exclusive. All processes or steps of the equipment are combined. Each feature disclosed in this specification (including accompanying claims, abstract and drawings) may be replaced by alternative features serving the same, equivalent or similar purpose, unless expressly stated otherwise.

Furthermore, those skilled in the art will appreciate that although some of the embodiments described herein include certain features, but not others, included in other embodiments, that combinations of features of different embodiments are intended to be within the scope of the invention within and form different embodiments. For example, in the following claims, any of the claimed embodiments may be used in any combination.

Various component embodiments of the present invention may be implemented in hardware, or in software steps running on one or more processors, or in a combination thereof. Those skilled in the art should understand that a microprocessor or a digital signal processor (DSP) may be used in practice to implement some or all functions of some or all components in the apparatus for creating a virtual machine according to the embodiment of the present invention. The present invention can also be implemented as apparatus or apparatus programs (eg, computer programs and computer program products) for executing part or all of the systems described herein. Such a program implementing the present invention may be stored on a computer-readable medium, or may be in the form of one or more signals. Such signals may be downloaded from Internet sites, or provided on carrier signals, or in any other form.

It should be noted that the above-described embodiments illustrate rather than limit the invention, and that alternative embodiments may be devised by those skilled in the art without departing from the scope of the appended claims. In the claims, any reference signs placed between parentheses shall not be construed as limiting the claim. The word "comprising" does not exclude the presence of elements or steps not listed in a claim. The word "a" or "an" preceding an element does not exclude the presence of a plurality of such elements. The invention can be implemented by means of hardware comprising several different elements and by means of a suitably programmed computer. In a step claim enumerating several means, several of these means can be embodied by one and the same item of hardware. The use of the words first, second, and third, etc. do not denote any order. These words can be interpreted as names.

The above description is only a preferred embodiment of the present invention, but the protection scope of the present invention is not limited to this. Substitutions should be covered within the protection scope of the present invention. Therefore, the protection scope of the present invention should be based on the protection scope of the claims.

Claims (4)

1. A method for verifying trustworthiness of a communication protocol, comprising:

performing lexical analysis, syntactic analysis and semantic analysis on the requirement specification meeting the safety transmission index to obtain an analysis result, describing the analysis result through a formal language, selecting a corresponding semantic abstract function, establishing the relationship between the formal description and a described object in an equivalence class, dividing the described object into a plurality of equivalence classes by using different semantic abstract functions, respectively establishing an abstract relationship between each equivalence class and different formal description languages, and integrating the formal description languages into the same semantic domain to obtain the requirement specification described by the formal language;

when a protocol is modeled, a model is endowed to each type of node, communication among the process models is described by using a process algebra description language, the simulation of scheduling frame information in a protocol period is completed by initializing a scheduling request of asynchronous frame information and modeling a scheduling algorithm in the protocol, and the whole protocol model is formed by the concurrence of processes of different types of nodes;

wherein, the requirements of the safe transmission index include: system interface requirements, user interface requirements, hardware interface requirements, software interface requirements, and communication interface requirements;

verifying the requirement specification described by the formal language through a formal verification tool to obtain a verification data set;

and performing specification detection according to the verification data set.

2. The method of claim 1, wherein the formal verification tool comprises:

process Analysis Toolkit (PAT).

3. The method of claim 1, wherein validating the data set comprises:

a correctness verification dataset, a completeness verification dataset, a consistency verification dataset, and a disambiguation verification dataset.

4. The method of claim 1, wherein said performing a specification test based on said validation dataset comprises:

verifying the data set according to the correctness, and detecting whether the specification is correct;

according to the completeness verification data set, detecting whether the specification is complete;

verifying the data set according to the consistency, and detecting whether the specifications are consistent;

and detecting whether the specification is unambiguous according to the unambiguous verification data set.

Images