CN103036739B - A Formal Method for Verification and Performance Analysis of Highly Reliable Communication Systems - Google Patents

Abstract

A formalized method for verification and performance analysis of high-reliability communication systems, comprising five major steps. This method is a method for formal verification and analysis of communication systems based on a combination of model checking and theorem proving. Based on a hypothesis-based approach, it proposes to establish an environmental state machine, perform hierarchical modeling of the design of network communication systems, formally verify key attributes, formalize high-order logic modeling of protocol transmission processes and attributes, and design and implement high-order logic formalization of the statistical characteristics of random variables. Based on the high-order logic model and related theorems established in HOL4, it implements automatic verification and quantitative dynamic performance analysis based on the formal model. This method has considerable practical value and broad application prospects in the field of formal verification engineering application technology.

Description

A Formal Method for Verification and Performance Analysis of Highly Reliable Communication Systems

technical field

The present invention relates to a formalized method for verification and performance analysis of highly reliable communication systems, which is an integrated implementation method of reliability verification (Reliability, Maintainability and Supportability, RMS for short) and performance analysis of embedded system communication, especially It is an integrated process construction method based on formal method verification and system quantitative performance analysis, and belongs to the technical field of formal verification engineering application.

Background technique

The communication system in the system-on-chip of many key applications usually has extremely high functional reliability, strict real-time and other requirements. There are countless examples of system-on-chip failures in critical applications resulting in significant loss of life and property; the traditional verification method for system-on-chip is testing or fault simulation, the main limitation of which is that it passes the test for a given data set, but it cannot be guaranteed in actual operation There are no errors in other inputs; and it is difficult to find potential unreasonable design or hidden errors of the system. How to ensure that the system satisfies the given functional and non-functional requirements has always been one of the key issues in the field of high-reliability on-chip computing. It is of great significance to verify the correctness and performance analysis of the communication system based on the formal method to ensure the correctness and reliability of the on-chip communication system. For the wide application of data transmission or concurrent and distributed processes in system-on-chip, the formal verification of the functional attributes of these applications usually adopts the method of model checking, but due to the low level of abstraction of the model checking method, only qualitative testing can be performed. If the abstraction is improper or the protocol is complex, it is easy to cause too many states, or even state explosion. At present, the formal method of network communication system only verifies its correctness, and if quantitative analysis is realized, it is carried out by establishing a simulation model.

Contents of the invention

1. Purpose: the purpose of this invention is to provide a kind of formalized method for verification and performance analysis of highly reliable communication systems, which is a method for formalized verification and analysis of communication systems based on model checking and theorem proof. Based on the method of hypothesis guarantee, the environment state machine is established, the design of the network communication system is modeled hierarchically, the key attributes are formally verified, and the transmission process of the protocol, the high-order logic formal modeling method of attributes, and the design Realize the formalization of high-order logic of statistical characteristics of random variables, and based on the high-order logic model and related theorems established in HOL4, realize automatic verification and quantitative dynamic performance analysis based on formal models.

2. Technical solution: In order to achieve the above purpose, the present invention provides a formalized method for verification and performance analysis of a highly reliable communication system. The specific steps of the method are as follows:

Step 1: Analyze the SOC function realization structure of the communication system, and extract the key functional modules; decompose and model the verification modules. Combining high-order logic theorem proving with symbolic model checking for combined formal verification.

Step 2: Realize the interface attributes, I/O ports and physical layer functions between modules, and use the method of model inspection to perform formal verification. Based on the symbolic model inspection platform, use the model inspection method to verify the relationship between modules hierarchically Realization of interface attributes, I/O ports and physical layer functions.

Step 3: Aiming at the problem that complex functional modules may cause too many states, carry out hierarchical abstraction, based on the hypothesis-guarantee theory, establish an environmental state machine model, and carry out combined verification strategies.

Step 4: Use the method of theorem proof to verify the logic and function realization of the data communication protocol and parallel application process. Formal expression of temporal properties and stochastic behavior of SoCs based on high-level logic;

Step 5: In the logical analysis expression analysis of the system, extract the mathematical logic form expression function of the statistical nature of the system process, and realize the dynamic quantitative performance analysis of the verification object process.

Among them, the "extracting key functional modules; performing verification module decomposition and modeling; combining high-order logic theorem proof and symbolic model checking to perform combined formal verification" described in step 1 is as follows: The modules of sending, receiving, link management, error control, and flow control in the communication system are extracted, and the verification modules are divided. Compared with the protocol design specifications, the verification goals and sub-goals are extracted. The modules with relatively independent functions are abstracted into separate verification components, and then the interface between low-coupling modules is abstracted into modeling and state description; the state machine model of the sending/receiving controller is established to form a formal model of system design, and the method of model checking is adopted authenticating. For the data transmission protocol and parallel distributed components and other processes, a high-level logic model is established on the HOL4 platform, and the method of theorem proof is used for verification.

Among them, the specific implementation process of the "hierarchical abstraction, based on the hypothesis-guarantee theory, the establishment of the environment state machine model, and the combined verification strategy" described in step three is as follows: For the problem of too many states generated during verification, the hypothesis-guaranteed reasoning method is used to abstract the environment state machine to verify the entire system in layers. Assume that the inference process is guaranteed as follows:

If two subsystems S1, S2 have properties: (1) S1 satisfies property P1 (2) when the environment of S2 satisfies property P1, S2 satisfies property P2. Then the combination S1||S2 of subsystems S1 and S2 satisfies property P2. The advantage of using this method for verification is that it is not necessary to verify the state machine established by the combination of S1 and S2, but only use S2 to verify P1, and then abstract P1 as the environment of S2 to verify P2. Assuming that P1 has much less state space than S1, it is beneficial to deal with large-scale circuit systems. Through the above steps, the present invention provides a method for formal verification and performance analysis of a communication system that combines two formal methods of model checking and theorem proving, and at the same time provides a method corresponding to a more general formal verification of a communication system process method.

3. Advantages and effects: The main advantage of the present invention is that it provides a formalized verification method for SOC communication systems at different levels of abstraction, and realizes performance analysis of system concurrency attributes. Realize the automatic verification technology of the correctness and reliability analysis of the communication system function of the more general SOC, so that the designer of the SOC can find the loopholes or logic errors in the system design stage at an early stage.

Description of drawings

Figure 1 The overall diagram of the implementation of the formal verification and analysis method of the communication system based on the combination of model checking and theorem proving

Fig. 2 is a flow chart diagram of the present invention

Figure 3 is a typical SOC system model verification and verification implementation process template

Figure 4 is the process template for proving the high-order logic theorem of a typical SOC system

Figure 5 is a state transition diagram of the sending control module

Detailed ways

In order to get a clearer understanding of the features and advantages of the present invention, a detailed description is given below in conjunction with the accompanying drawings: FIG. 1 depicts the overall architecture of the present invention.

When SOC designers verify the behavior and function correctness of the designed or implemented on-chip communication system, a formal verification method of the present invention can realize the attribute verification of the system at different levels of abstraction and based on the established formal model, carry out Performance analysis:

See Fig. 2, a kind of formalized verification method that is used for high reliable communication system performance inspection and analysis of the present invention, its specific implementation steps are:

Step 1: Analyze the system design and perform verification decomposition. As shown in Figure 2, the verification tasks are decomposed according to system functions and implementation characteristics.

(1) Analyze the attributes, function descriptions and realization of each key module or process in detail, extract the verification goals and sub-goals,

(2) Carry out the division of system function modules and the abstraction of verification attributes, abstract the modules with relatively independent functions into separate verification components, and then carry out abstract modeling and state description of the interface between low-coupling modules, and establish an abstract state machine.

(3) Establish high-level logic models for processes such as data transmission protocols and parallel distributed components, and use the method of theorem proof to verify,

(4) For components with relatively independent functions and interfaces between low-coupling modules, this project intends to use the method of model checking for verification.

Step 2: Realize the interface properties, I/O ports, and physical layer functions between modules, and use the model inspection method to perform formal verification. Based on the symbolic model inspection platform, use the model inspection method to verify the interfaces between modules in layers Realization of attributes, I/O ports and physical layer functions. The process of model verification includes three processes of modeling, property description and automatic verification. As shown in Figure 3, the system realization of the verification object module is abstracted and formally expressed, and the finite state of the system is represented by the Kripke structure of 5-tuple Space; use computational tree temporal logic (CTL) to describe the expected attributes of the system. This process requires accurate description and avoids ambiguity. Use the symbolic model verification tool SMV (Symbolic Modeling Verifier) to automatically exhaustively prove whether the expected properties are established in the state space, and if it is established, it means that the design and implementation meet the expected properties. If not, output a counterexample, and then locate the error based on the simulation test. This can be a cyclical process of verification→error reporting→error message analysis and model modification→revalidation. For example, in Figure 5, the transmitter is in the waiting state in the reset state, (1) If the Tick_IN (request to send timecode) signal from the host system is high, and the ESC signal has been sent (that is, the ESC_Gone_internal signal is high), then The transmitter will reach the locked time code state (in this state, Provide_TimeCode is set to 1 and sent to the send register sub-module), and then unconditionally arrives at the send time code state. (2) If Send_FCT (from the control module) is 1 and EightMore= 1 (indicating that the receiver has more than 8 spaces to store data) and ESC_Gone_internal=0 (if ESC_Gone_internal=1, then ESC+FCT is a null character), then the transmitter will reach the lock flow control flag state (in this state Set Provide_FCT to 1 and send it to the sending register submodule), and then unconditionally reach the state of sending constant characters. (3) If Send_NULL (from the control module) = 1 and ESC_Gone_internal = 1, then the transmitter will reach the lock flow control flag state (in this state, Provide_FCT is set to 1 and sent to the transmit register submodule). (4) If Send_All (from the control module) = 1 and NoCredit = 0, then the transmitter will reach the lock flow control flag state (in this state, Provide_ESC is set to 1 and sent to the send register sub-module). (5) If Send_EEP=1, then the transmitter will reach the state of locking the end of the error packet (in this state, Provide_EEP is set to 1 and sent to the sending register sub-module). (6) If Send_EOP=1, then the transmitter will reach the state of locking the correct packet end flag (in this state, Provide_EOP is set to 1 and sent to the sending register sub-module). (7) If Send_NChar_Flag=1, then the transmitter will reach the locked constant character state (in this state, Provide_NChar is set to 1 and sent to the send register submodule).

The meaning of some of the main input variables in the figure:

1 The protocol specification must meet mutual exclusion, because there is a problem of priority, so it is impossible to send time code, constant character and flow control flag at the same time.

Property 1: assert G~(!TX_Reset&Provide_TimeCode&Provide_NChar&Provide_FCT);

2 There is a priority relationship between the characters sent, so the issue of priority must be verified. Property 2 means that when the time code and FCT are to be sent at the same time, the time code is sent first.

Property2:SPEC AG(!TX_Reset&TX_ClockEnable&(Tick_IN&ESC_Gone_internal)&(Send_FCT&EightMore&!ESC_Gone_internal)->AF Provide_TimeCode);

3 According to the protocol specification, the nature to be verified mainly involves whether each state in the state transition can enter the corresponding state after the conditions are met and whether the output signal in the corresponding state meets the requirements of the protocol specification. A total of 7 branch tenses are extracted according to the requirements The nature of logical formulas.

Property3:SPEC AG(AG Send_NChar_Flag->AF present_state=1&AF present_state=2&AF Provide_NChar&AF NCharOnTrip&AF DCReg_Read);

Property4:SPEC AG(AG ESC_Gone_internal->AF present_state=3&AF present_state=4&AF Provide_TimeCode);

Property5:SPEC AG(AG Send_FCT->AF present_state=5&AF present_state=9&AFpresent_state=10&AF Provide_FCT);

Property6:SPEC AG (AG Send_EOP->AF present_state=6&AF present_state=9&AFpresent_state=10&AF Provide_EOP&AF DCReg_Read&AF NCharOnTrip);

Property7:SPEC AG(AG Send_EEP->AF present_state=7&AF present_state=9&AFpresent_state=10&AF Provide_EOP&AF DCReg_Read&AF NCharOnTrip);

Property8: SPEC AG (AG Send_NULL->AF_present_state=8&AF present_state=9&AFpresent_state=10&AF Provide_ESC);

The formulas Property3 to Property8 in the above part mainly verify whether the control module can enter the corresponding state and output the corresponding sending control signal in this state after the sending request enters the sending control module, and whether it can return to the reset state after entering these states. Reset the initial state.

Property9:SPEC AG(AG(!ESC_Gone_internal&Send_FCT&EightMore&present_state=5)->AF EightMoreAcknowledge);

The branch temporal logic formula Property9 expresses that the receiving buffer of host A still has space to receive data, and requests to send a flow control character FCT to host B at the sending end, and the sending control module of host A at the end of A will generate a flow control character that can receive more than eight The confirmation control code of the constant character is sent to the register of the transmitter, and finally sends an FCT identifier to the host.

Step 3: After verifying the local attributes of each module separately, it is necessary to check the global attributes of the combination of modules. When verifying the complex functional attributes formed by cascade coupling of multiple modules, there will be problems such as too many states. The reasoning method based on hypothesis guarantee is used to abstract, establish the environment state machine, and make the verification object communicate with the environment state machine. For example, the sender/receiver buffer is abstracted into a memory interface for data characters, etc. In the connected state, the data and filtered signals output by the transmitter should conform to the DS code. If the value of two consecutive bits of the data signal is the same, the state of the filtered signal changes when the next bit is transmitted, otherwise the filtered signal remains unchanged during the two bit times. The premise of this property is that the flow control signal Provide_FCT is true, which is controlled by the controller. Therefore, an assumption about the environment P1 is added. In the connection state, one of the link keep-alive and flow control labels must be true. Only in this way can Provide_FCT be true in this state. Through verification, the controller N satisfies the property P1, and then the transmitter module is embedded in the environment satisfying the above assumptions, and the correctness of the property can be checked by the method of model verification. And avoid the problem of too much state.

Step 4: Theorem proving is to deduce the properties of the system based on the axioms of the formal logic system. It can rely on structured induction techniques to prove on infinite fields, and can directly deal with infinite state spaces, which can greatly reduce the number of states that a model checker needs to analyze. The high-order logic theorem prover HOL4 has the characteristics of strong expression ability and type polymorphism, and already has a considerable basic theorem library embedded in ML functions. Using HOL4 can verify the attributes of the modules divided in the first step above. The basic process As shown in Figure 4, the formalized model to be verified is input into HOL in the form of a goal, and the model can be divided into sub-goals interactively in HOL. The proof checking system of HOL4 will automatically check the proof process of each sub-task. Correctness. In this process, the new theorems and descriptions we need to use must first be established as formal models and added to HOL4. The added theorems are reusable, which is very convenient. Formal verification for reusability and modularity. This project intends to formally describe the variance and other statistical properties of discrete random variables, first establish a formal model and add it to HOL4; complete the proof of the variance properties required for the subsequent quantitative description of random properties and performance analysis, and add it to HOL4 as a theorem .

Establish the logical model of the transmission protocol in HOL4, and conduct reasoning verification:

1) In HOL4, define data types for transmission data information, control information, transmission time, and number of packets;

2) Establish high-order logical predicate (function) expressions for the sending and receiving processes of the channel and the communication parties respectively;

Step 5: Formally express the initial conditions and constraints of the protocol in HOL4, and express them as disjunctive expressions with the predicate function in the fourth step. The transmission protocol judges whether the data is transmitted correctly by using whether the time from sending the data packet to receiving the confirmation message is within the expected range, and uses the error plus retransmission mechanism for error correction. If the probability of error is p, and the number of channel retransmissions is exponentially distributed, the data transmission delay can be expressed as:

D=t _r +d _tran +d _prog +(t _r +t _timer )(G _(1p) -1)

t _r : resend data time,

t _timer : the time from when the sender finishes sending the data packet to the timeout,

d _tran : the time required for data packet transmission

d _prog : signal propagation delay between nodes

If G _x in the above formula obeys the Gaussian distribution random variable, the probability of successful transmission is x.

Then the average delay of transmitting a data packet can be expressed as:

((t _r +t _timer )p/(1-p))+t _r +d _tran +d _prog : Use the random variable and its statistical attribute theorem in HOL4 to express and extract the protocol delay, and realize the performance analysis .

Claims (1)

1. A formalized method for verification and performance analysis of a highly reliable communication system, characterized in that: the specific steps of the method are as follows: Step 1: Analyze the SOC function realization structure of the communication system, extract key functional modules, decompose and model the verification modules, combine high-order logic theorem proofs with symbolic model verification, and perform combined formal verification; Step 2: Realize the interface attributes, I/O ports and physical layer functions between modules, and use the method of model inspection to perform formal verification. Based on the symbolic model inspection platform, use the model inspection method to verify the relationship between modules hierarchically Realization of interface attributes, I/O ports and physical layer functions; Step 3: In view of the problem that complex function modules may cause too many states, perform hierarchical abstraction, based on the assumption-guarantee theory, establish an environmental state machine model, and carry out combined verification strategies; Step 4: Use the method of theorem proof to verify the logic and function realization of the data communication protocol and parallel application process; formally express the temporal properties and random behavior of the system on chip based on high-order logic; Step 5: In the logical analysis expression analysis of the system, extract the mathematical logic form expression function of the statistical nature of the system process, and realize the dynamic quantitative performance analysis of the verification object process; Among them, in step 1, "extract key functional modules, perform verification module decomposition and modeling, combine high-order logic theorem proof and symbolic model inspection, and perform combined formal verification;" the specific implementation process is as follows: Extract the sending, receiving, link management, error control, and flow control modules in the communication system, divide the verification modules, and extract the verification goals and sub-goals according to the protocol design specifications; the modules with relatively independent functions are abstracted into separate verification components , and then carry out abstract modeling and state description of the interface between low-coupling modules; establish the state machine model of the sending/receiving controller, form a formal model of system design, and use the method of model checking to verify; the data transmission protocol and parallel The distributed component process is built on the HOL4 platform to establish a high-level logic model, which is verified by the method of theorem proof; Among them, the specific implementation process of the "hierarchical abstraction, based on the hypothesis-guarantee theory, the establishment of the environment state machine model, and the combined verification strategy" described in step three is as follows: For the problem of too many states generated during verification, adopt the method of hypothesis-guaranteed reasoning, abstract the environment state machine, and verify the whole system in layers; the process of hypothesis-guaranteed reasoning is as follows: If two subsystems S1 and S2 have attributes: ( 1) S1 satisfies property P1; (2) when the environment of S2 satisfies property P1, S2 satisfies property P2; then the combination of subsystems S1 and S2 S1||S2 satisfies property P2; the advantages of using this method for verification are: It is not necessary to verify the combination of S1 and S2 to establish a state machine, just use S2 to verify P1, and then abstract the assumption that P1 is the environment of S2 to verify P2; assuming that P1 has a much smaller state space than S1, it is beneficial to deal with large Scale circuit system.