CN109976712A - One kind doing formalization verification method to network physical system requirements based on UPPAAL-SMC - Google Patents

Abstract

The invention discloses a method for formal verification of network physical system requirements based on UPPAAL-SMC, which includes expressing a demand model of a network physical system CPS in an EAST-ADL architecture model in the form of a probabilistic clock constraint specification language; It parses and generates an abstract syntax tree AST; traverses the abstract syntax tree AST to extract the key information of each relation or expression statement in the PrCCSL statement, and matches the corresponding template for each relation or expression statement according to the content of the key information to generate the STA model and its query, generate the STAs model and save it as a STAs file, input the STAs file into the integrator, integrate the system behavior model of the cyber-physical system, output the verifiable Net‑STA model, and call the verifiable Net‑STA model to the UPPAAL‑SMC model Formal verification engine Verifyta; Query generator outputs the current query verification statement to Verifyta, and starts Verifyta to perform formal verification. The present invention formally verifies the requirements based on the probabilistic description of the network physical system requirements by PrCCSL and UPPAAL-SMC.

Description

A Formal Verification Method for Cyber-Physical System Requirements Based on UPPAAL-SMC

technical field

The invention relates to the field of data processing, in particular to a formal verification method for network physical system requirements based on UPPAAL-SMC.

Background technique

The modeling and analysis of functional and non-functional requirements, such as timing constraints, energy constraints, etc., are crucial for Cyber-Physical Systems (CPS, Cyber-Phsical System). EAST-ADL (Electronic Architecture and Software Tools-Architecture Description Language, Architecture Description Language) is a domain-specific architecture language for security-critical cyber-physical system design. The Probabilistic Clock Constraint Specification Language (PrCCSL, Probability extension CCSL) is a probabilistic extension of the Clock Constraint Specification Language (CCSL, Clock Constraint Specification Language). The timing constraints of the EAST-ADL architecture model are described by the PrCCSL language with probabilistic semantics, and then the semantics of the PrCCSL statements are converted into the Stochastic Timed Automata (STAs, Stochastic Timed Automata) model of the statistical model checking tool UPPAAL-SMC. Model checking.

In the context of EAST-ADL, many people have studied the integration of EAST-ADL with formal verification based on timing constraints, but they are limited to the execution of system functions without considering how to deal with the random behavior of the system. The execution semantics of the controllers and environments of cyber-physical systems have been defined in PrCCSL and then mapped to the UPPAAL-SMC model for probabilistic model checking. It has been proposed to use CCSL with probabilistic logic timing to realize the stochastic analysis of hybrid systems by limiting the possibility of events. Currently, these methods lack supporting tools to implement their formal verification and simulation methods. Someone provides a tool TimePF for modeling and formal verification of timing constraints in CCSL. Some people use TimePF to describe the temporal properties of cyber-physical systems with CCSL, and interpret CCSL statements with linear temporal logic (LTL, Linear temporal logic) with operational semantics as a finite state machine for scheduling analysis. In contrast to current inventions, these methods lack an accurate description of randomness, especially regarding the randomness behavior of continuous dynamic systems at different clock rates during execution.

SUMMARY OF THE INVENTION

The main purpose of the present invention is to propose a formal verification method for network physical system requirements based on UPPAAL-SMC, in order to overcome the above problems.

In order to achieve the above-mentioned purpose, a kind of formal verification method based on UPPAAL-SMC that the present invention proposes to network physical system requirements, comprises the following steps:

S10 uses the probabilistic clock constraint specification language PrCCSL in the editor to formally represent the demand model of the cyber-physical system CPS in the EAST-ADL architecture model, and generate PrCCSL statements;

S20 inputs the PrCCSL statement into the parser, and parses it to generate an abstract syntax tree AST;

S30 traverses the abstract syntax tree AST to extract key information of each relation or expression statement in the PrCCSL statement, and matches the corresponding template for each relation or expression statement according to the content of the key information to generate an STA model and its query statement. Generate the STAs model, save the STAs model as a STAs file in .xml format, and generate a Query generator for the query statement;

S40 inputs the STAs file into the integrator, integrates the system behavior model of the cyber-physical system, and outputs a verifiable Net-STA model;

S50 calls the verifiable Net-STA model to the formal verification engine Verifyta of the UPPAAL-SMC model; the Query generator outputs the current query verification statement to Verifyta, and starts Verifyta to perform formal verification.

Preferably, the CPS cyber-physical system model in the EAST-ADL architecture includes a system architecture model and a requirement model, wherein the system behavior in the system architecture model is represented by a functional prototype, and the S10 further includes:

S01 cyber-physical system is modeled using EAST-ADL architecture model, output system architecture model and requirement model, continuous or discrete system behavior of each functional prototype of the system architecture model is modeled by UPPAAL-SMC model, each functional prototype Corresponding to a time automata STA model, the system behavior of the cyber-physical system is represented as a Net-STA model, which is saved as a system model file in .xml format.

Preferably, after the S10 and before the S20, the steps further include:

S02 uses BNF language to describe the grammar of PrCCSL, calls the parser generation tool ANTLR, and constructs the parser.

Preferably, after the S20 and before the S30, the steps further include:

S03 checks whether the abstract syntax tree AST has grammatical errors, if not, enter S30, if so, return to S10.

Preferably, the conversion mode includes PrCCSL mode and PrCCSL+System mode, and the step of saving the STAs model as a STAs file in the .xml format in described 30 includes:

S301 Input the STAs model into the converter to obtain the user's formal verification requirements;

S302 If the user verification requirement is obtained, select the PrCCSL+System mode, input the STAs model into the integrator to integrate the system behavior model of the cyber-physical system, and save the output result of the integrator as a verifiable STAs file in .xml format; if If the user authentication requirements are not obtained, select the PrCCSL mode and save the STAs model as a STAs file in .xml format.

Preferably, the corresponding templates matched to each relation or expression statement according to the content of the key information include relation templates and expression templates.

Preferably, the query statement includes five query statements, namely hypothesis testing, probability estimation, simulation, expected value and probability comparison, and the Query generator includes at least the above five query statements and configuration parameters thereof.

Preferably, the demand model of the cyber-physical system CPS includes a functional demand model and a non-functional demand model, and the method of S10 is specifically: using the mutual exclusion, equivalence and sub-clock three of the PrCCSL language for the functional demand of the cyber-physical system CPS The non-functional requirements of the cyber-physical system CPS are expressed by the priority and causal relations or expression statements of the PrCCSL language.

Preferably, it also includes S60 calling XML DOM in Python to parse the .xml file to generate the STA model, and using Tkinter, a library of built-in graphical development interface in Python, to implement a mapping template for each PrCCSL statement.

The invention also discloses a formal verification tool for network physical system requirements based on UPPAAL-SMC, including:

System modeling module for cyber-physical system modeling using EAST-ADL architecture model, output system architecture model and requirement model, continuous or discrete system behavior of each functional prototype of the system architecture model is modeled by UPPAAL-SMC model. Each functional prototype corresponds to a time automaton STA model, so the system behavior of the cyber-physical system is represented as a Net-STA model, which is saved as a system model file in .xml format;

The presentation module is used to formally represent the requirement model of the cyber-physical system CPS in the EAST-ADL architecture model using the probabilistic clock constraint specification language PrCCSL in the editor of the probabilistic clock constraint specification language converter ProTL, and generate the PrCCSL statement;

The construction module is used to describe the grammar of PrCCSL using the BNF language, call the parser generation tool ANTLR, and construct the grammar parser of the PrCCSL language;

The parsing module is used to input the PrCCSL statement into the parser, and parse to generate the abstract syntax tree AST;

The grammar check module is used to check whether the abstract syntax tree AST has any grammar errors. If not, it will enter the generation module. If there is, it will return to the representation module;

The generation module is used to traverse the abstract syntax tree AST to extract the key information of each relationship or expression statement in the PrCCSL statement, and match the corresponding template for each relationship or expression statement according to the content of the key information to generate the STA model and its query statement. Several STA models generate STAs models, the STAs models are saved as STAs files in .xml format, and the query statement generates a Query generator. The generation module includes a mode conversion sub-module for inputting the STAs model into the converter to obtain user Formal verification requirements, if the user verification requirements are obtained, select the PrCCSL+System mode, input the STAs model into the integrator to integrate the system behavior model and the STAs model of the cyber-physical system, and save the output of the integrator in .xml format as Verifiable STAs file; if user authentication requirements are not obtained, select PrCCSL mode and save the STAs model as a STAs file in .xml format;

The integration module is used to input the STAs file into the integrator, integrate the system behavior model of the cyber-physical system, and output a verifiable Net-STA model;

The verification execution module is used to import the verifiable Net-STA model into the verifier, and call the formal verification engine Verifyta of the UPPAAL-SMC model; the Query generator outputs the current query verification statement to Verifyta, and starts Verifyta to perform formal verification.

The present invention develops an automatic conversion tool ProTL, from the probabilistic clock constraint specification language to the verifiable random time automata model, and can generate Hypothesis Testing, Probability Estimation, Simulations, Expected Value (Expected Value), Probability Comparison (Probability Comparison) and other five query statements are used for formal verification and system simulation of system requirements. ProTL also provides visual images showing simulation results and error backtracking and generating counter-examples. The present invention is the first tool for formal verification of requirements based on the probabilistic description of network physical system requirements by PrCCSL and UPPAAL-SMC.

Description of drawings

In order to explain the embodiments of the present invention or the technical solutions in the prior art more clearly, the following briefly introduces the accompanying drawings that need to be used in the description of the embodiments or the prior art. Obviously, the accompanying drawings in the following description are only These are some embodiments of the present invention, and for those of ordinary skill in the art, other drawings can also be obtained according to the structures shown in these drawings without creative efforts.

FIG. 1 is a flow chart of a method according to an embodiment of the present invention;

Fig. 2 is the template that the equivalent relation or expression statement of PrCCSL is mapped to STA model;

Figure 3 is a template for mapping the mutually exclusive relationship or expression statement of PrCCSL to the STA model;

Fig. 4 is the template that the sub-clock relation or expression statement of PrCCSL is mapped to STA model;

Fig. 5 is the template that the causal relation or expression statement of PrCCSL is mapped to the STA model;

Fig. 6 is the template that the priority relation or expression statement of PrCCSL is mapped to STA model;

Fig. 7 is the template that PrCCSL conditional expression statement is mapped to STA model;

Fig. 8 is the template that PrCCSL delay expression statement is mapped to STA model;

Fig. 9 is the template that PrCCSL filter expression statement is mapped to STA model;

Figure 10 is a template for mapping the PrCCSL infimum expression statement to the STA model;

Fig. 11 is the template that the PrCCSL supremum expression statement is mapped to the STA model;

Fig. 12 is the template that PrCCSL periodic expression statement is mapped to STA model;

Fig. 13 is the template that PrCCSL intersection expression statement is mapped to STA model;

Fig. 14 is the template that PrCCSL union expression statement is mapped to STA model;

Figure 15 is the visualization converter of ProTL;

Figure 16 is the visual validator of ProTL,

The realization, functional characteristics and advantages of the present invention will be further described with reference to the accompanying drawings in conjunction with the embodiments.

Detailed ways

The technical solutions in the embodiments of the present invention will be clearly and completely described below with reference to the accompanying drawings in the embodiments of the present invention. Obviously, the described embodiments are only a part of the embodiments of the present invention, not all of the embodiments. Based on the embodiments of the present invention, all other embodiments obtained by those of ordinary skill in the art without creative efforts shall fall within the protection scope of the present invention.

It should be noted that if there are directional indications (such as up, down, left, right, front, back, etc.) involved in the embodiments of the present invention, the directional indications are only used to explain a certain posture (as shown in the accompanying drawings). If the specific posture changes, the directional indication also changes accordingly.

In addition, if there are descriptions involving "first", "second", etc. in the embodiments of the present invention, the descriptions of "first", "second", etc. are only used for the purpose of description, and should not be construed as indicating or implying Its relative importance or implicitly indicates the number of technical features indicated. Thus, a feature delimited with "first", "second" may expressly or implicitly include at least one of that feature. In addition, the technical solutions between the various embodiments can be combined with each other, but must be based on the realization by those of ordinary skill in the art. When the combination of technical solutions is contradictory or cannot be realized, it should be considered that the combination of such technical solutions does not exist. , is not within the scope of protection required by the present invention.

As shown in Figure 1-16, a method for formal verification of cyber-physical system requirements based on UPPAAL-SMC proposed by the present invention includes the following steps:

S10 uses the probabilistic clock constraint specification language PrCCSL in the editor to formally represent the EAST-ADL requirement model of the cyber-physical system CPS, and generate PrCCSL statements;

S20 inputs the PrCCSL statement into the parser, and parses it to generate an abstract syntax tree AST;

S30 traverses the abstract syntax tree AST to extract key information of each relation or expression statement in the PrCCSL statement, and matches the corresponding template for each relation or expression statement according to the content of the key information to generate an STA model and its query statement. Generate the STAs model, save the STAs model as a STAs file in .xml format, and generate a Query generator for the query statement;

S40 inputs the STAs file into the integrator, integrates the system behavior model of the cyber-physical system, and outputs a verifiable Net-STA model;

The S50 verifiable Net-STA model is imported into the verifier, and the formal verification engine Verifyta of the UPPAAL-SMC model is called; the Query generator outputs the current query verification statement to Verifyta, and starts Verifyta to perform formal verification.

In the embodiment of the present invention, the present invention develops a tool ProTL (Probabilistic-CCSL TransLator, Probabilistic Clock Constraint Specification Language Translator) that can be automatically converted to provide automatic conversion from PrCCSL sentences to UPPAAL-SMC models. From the probabilistic clock constraint specification language to the verifiable random time automata model, import the ProTL verifier, which calls the formal verification engine Verifyta of the UPPAAL-SMC model, to the constraints of the probabilistic timing and causality described by PrCCSL /Requires verification. ProTL provides a text editor for PrCCSL statements, and generates different probabilistic query statements in the Query generator.

Save the STAs model in .xml format to be recognized by UPPAAL-SMC.

For example: a relation or expression statement a subclock(p=0.96)b; the key information is that a is a clock. b is a clock, and subclock is a subclock relation (Relation) statement. Suppose the current query statement entered, such as Pr[ <=1000]([]not cauObs43.fail)>=0.96. Among them, 1000 is bound, cauObs43 is the subclock relationship or the name of the STA generated by the expression statement in the xml file, and 0.96 is the probability.

In addition, in order to facilitate the analysis of the constraints and requirements described by PrCCSL, ProTL calls the formal verification engine "verifyta" of UPPAAL-SMC as its verification backend, which provides verification and simulation capabilities for the transformed model; ProTL also provides visual image display Simulation results and error backtracking and generation of counterexamples.

The implementation method of ProTL:

Use ProTL to formally analyze the functional requirements and non-functional (timing, energy consumption) requirements of the Cyber-Physical System (CPS, Cyber-Physical System) in EAST-ADL,

The method consists of the following steps:

(1) Modeling the system behavior and requirements of CPS with EAST-ADL: The entry point of our method is to first use EAST-ADL to model the system architecture, in which the system behavior is represented by a function prototype (FunctionPrototype), here Based on UPPAAL-SMC, the dynamic or continuous behavior of each FunctionPrototype is described in detail. The (non-)functional requirements of the system are modeled using ESAT-ADL's Timing Model. As shown in Figure 1, the behavior of each FunctionPrototype in EAST-ADL is modeled as the corresponding STA by UPPAAL-SMC, and the behavior of the entire system is finally represented as a parallel system composed of the Net-STA model.

(2) Use PrCCSL to describe the (non) functional requirements of the system in ProTL: requirements in EAST-ADL (including functional requirements, and non-functional requirements, such as timing constraints and energy constraints). Usually, functional requirements are It is specified as a logical relationship, that is, mutual exclusion, coincidence and subclock three relationships (PrCCSLRelation). Functional and non-functional requirements are specified as temporal relationships, namely precedence and causality (PrCCSL Relation). In order to analyze the energy consumption constraints of the system, the energy consumption is represented by the dense clock type (DenseClockType) extended by the dense clock.

(3) Using ProTL to convert PrCCSL statements into verifiable UPPAAL-SMC models: ProTL converts PrCCSL statements (stored in ".txt" files) into STA models. The system behavior model represented by UPPAAL-SMC (stored in ".xml" file) can be imported into ProTL, which integrates the imported model and the generated STA model into a verifiable UPPAAL-SMC model.

Formal verification and simulation of the generated model with ProTL: ProTL can generate different types of query (Query) statements for verification and simulation. Visual analysis images are also provided to display analysis results.

The ProTL architecture can be divided into two main components, namely the Translator and the Verifier

The converter provides an editor for editing the text encoding of PrCCSL statements and stores the encoding in a ".txt" file. The conversion from PrCCSL sentences to STA is achieved by using the parser generation tool ANTLR

Completed. ANTLR is a parser generator that automatically constructs a lexical parser by analyzing the Backus-Naur From (BNF) grammar of a programming language. We describe the grammar of PrCCSL in BNF and then call ANTLR to generate a lexer that can parse PrCCSL sentences. The parser reads the PrCCSL statement to generate an abstract syntax tree (AST, Abstract Syntax Tree), which is an intermediate form with a "tree" data structure. By traversing the AST, we extract the information (i.e., operators and parameters) of the PrCCSL statement and match the transformation patterns to generate the corresponding UPPAAL-SMC model based on the extracted information. Conversion offers two conversion modes. Generate different output results in different modes:

(1) PrCCSL mode: The converter converts PrCCSL statements into STA and query statements and saves them as a .xml file;

(2) PrCCSL+System mode: The converter converts the PrCCSL statement into STA and query statement, and uses the Integrator to integrate the imported system model (".xml" file) and the corresponding STA of the PrCCSL statement into one in the verifiable .xml file.

The validator provides a Query generator for generating UPPAAL-SMC query statements and an interface for displaying the validation results. As shown in Figure 1. The verifier provides verification and simulation capabilities for the transformed model by calling the formal verification engine verifyta of UPPAAL-SMC as its verification backend. output file) and the generated queries perform formal verification and simulation. In addition, the analysis results of the combined model can be traced back to the original PrCCSL encoding, i.e., it can reflect the correctness (or incorrectness) of the input sentence. During the verification process, if the PrCCSL statement does not meet the requirements and constraints of the system, ProTL generates a simulation image that provides diagnostic information to trace the source of the error. The error may appear in:

(1) In the editor, use the requirements described by PrCCSL;

(2) The Net-STA model generated by modeling the behavior of the system with UPPAAL-SMC;

(3) The demand model of the CPS system described by EAST-ADL;

(4) The architecture model of the CPS system described by EAST-ADL.

Preferably, the CPS cyber-physical system model in the EAST-ADL architecture includes a system architecture model and a requirement model, wherein the system behavior in the system architecture model is represented by a functional prototype, and the S10 further includes:

S01 cyber-physical system is modeled using EAST-ADL architecture model, output system architecture model and requirement model, continuous or discrete system behavior of each functional prototype of the system architecture model is modeled by UPPAAL-SMC model, each functional prototype Corresponding to a temporal automata STA model, the system behavior of the cyber-physical system is represented as a Net-STA model, and the system model file is saved in .xml format.

Preferably, after the S10 and before the S20, the steps further include:

S02 uses BNF language to describe the grammar of PrCCSL, calls the parser generation tool ANTLR, and constructs the parser.

In the embodiment of the present invention, the function of the parser is to parse the PrCCSL statement into an abstract syntax tree (AST). We then traverse the AST using the observer pattern so that we can reconstruct the semantics and decide which mapping template should be matched. The first step in building the parser is that we need to define the BNF grammar for the ProTL input language.

Based on the proposed extend-BNF grammar, we construct the extend-BNF grammar of PrCCSL to parse sentences. ANTLR is a multi-domain parser generator that combines the flexibility of hand-coded parsing with the convenience of a parser generator. An AST is generated for each PrCCSL statement in order to traverse the AST and match the map template, so we implement the observer pattern in Python as a listener to traverse the AST to reconstruct the semantics of the PrCCSL statement and match the map template. The Observer pattern is a software design pattern in which an object called a principal maintains a list of its dependencies, called observers, and automatically notifies them of any state changes, usually by calling one of its methods. Listeners are capable of responding to specific rule entry and exit events (ie, recognizing certain phrases), which are triggered by AST traversal when starting and completing a visit to a node, respectively. Example: parse the following PrCCSL, the AST of the {supctrl clockDef periodicOn c1period 50;} statement.

When ProTL parses the statement into AST, the listener calls the exitPara() function to match the para rule and records <Int>=50, the exitCe() function matches the first ce rule and records <Clock>=c1, and exitEr( ) function matches the fourth cr rule and records <Clock>=supctrl. So this statement can match the periodicOn mapping template, where the arguments are a new Clock suptrcl, base Clock c1 and period is 50 to generate the associated random automaton model.

Preferably, after the S20 and before the S30, the steps further include:

S03 checks whether the abstract syntax tree AST has grammatical errors, if not, enter S30, if so, return to S10.

Preferably, the conversion mode includes PrCCSL mode and PrCCSL+System mode, and the step of saving the STAs model as a STAs file in the .xml format in described 30 includes:

S301 Input the STAs model into the converter to obtain the user's formal verification requirements;

S302 If the user verification requirement is obtained, select the PrCCSL+System mode, input the STAs model into the integrator to integrate the system behavior model of the cyber-physical system, and save the output result of the integrator as a verifiable STAs file in .xml format; if If the user authentication requirements are not obtained, select the PrCCSL mode and save the STAs model as a STAs file in .xml format.

In the embodiment of the present invention, ProTL provides two conversion modes, and different output results are generated in different modes. PrCCSL mode: ProTL converts the input PrCCSL statements into STAs and query statements, and the generated model is saved as an .xml file that can be recognized by UPPAAL-SMC, which contains all the generated STAs and query statements.

PrCCSL+System mode: ProTL automatically integrates the system model (provided by the user) with the STAs and query statements generated by the input PrCCSL statement into a .xml file, and then the user clicks the Verify button, and ProTL formally verifies whether the system model satisfies its requirements. Functional and non-functional requirements, and output feedback information.

Preferably, the corresponding templates matched to each relation or expression statement according to the content of the key information include relation templates and expression templates, the relation templates include equality, mutual exclusion, sub-clock, causality, and priority relation templates, and the expression templates include conditional , delay, filter, infimum, supremum, period, intersection, union expression templates.

Preferably, the query statement includes five query statements, namely hypothesis testing, probability estimation, simulation, expected value and probability comparison, and the Query generator includes at least the above five query statements and configuration parameters thereof.

In this embodiment of the present invention, the present invention generates at least five query statements: Hypothesis Testing, Probability Estimation, Simulations, Expected Value, and Probability Comparison System requirements for formal verification and system simulation.

Preferably, the demand model of the cyber-physical system CPS includes a functional demand model and a non-functional demand model, and the method of S10 is specifically: using the mutual exclusion, equivalence and sub-clock three of the PrCCSL language for the functional demand of the cyber-physical system CPS The non-functional requirements of the cyber-physical system CPS are expressed by the priority and causal relations or expression statements of the PrCCSL language.

Preferably, it also includes S60 calling XML DOM in Python to parse the .xml file to generate the STA model, and using Tkinter, a library of built-in graphical development interface in Python, to implement a mapping template for each PrCCSL statement.

In the embodiment of the present invention, the practical example:

1. Represents Template

Template Template in the UPPAAL-SMC model represents an STA, which has two properties: Name and Parameter. Maps the source code of the .xml file of its properties to the Python source code of its properties. We start by creating the Template node and inserting it into the root of the .xml file. Then we create a Name node and assign it to ITE to represent the Template Name in STA. Create a para node with a Text node representing the Parameter in STA. Location is the basic element of STA, it has three basic properties: x, y and id.

2. Indicates Location

Location is the basic element of STA. It has three basic properties: x, y and id. The attribute Name is optional, we create a Location node and assign values to the attributes x, y, and id. If the Location is committed, we need to create a node named committed and insert it below the Location node. Then create an init node to represent the initial Location.

3. Represents Transition

Transition has Source Location, target location and label. There are three types of label: synchronization, assignment, guard. For each Transition, we first create a Transition node, and then set the ID of its source Location and target Location. For different types of Labels, create a Label node and set the x,y,kind properties. Transtion may also contain a nail attribute, we construct a nail node with position information to represent it.

In a similar way, we can implement all mapping templates.

In the embodiment of the present invention, the Query generator of the present invention is developed by Tkinter, a library of built-in graphical development interface in Python, and provides a set of user-friendly functions, including a query statement with customizable configuration parameters, and a visual data image of the analysis result, And generate counter-examples through validation failures to provide diagnostic information to help users find the problem. Tkinter is a standard GUI (Graphical User Interface) package for Python, we use Tkinter to design the GUI interface of ProTL.

The invention also discloses a formal verification tool for network physical system requirements based on UPPAAL-SMC, which is used to realize the above method, which includes:

System modeling module for cyber-physical system modeling using EAST-ADL architecture model, output system architecture model and requirement model, continuous or discrete system behavior of each functional prototype of the system architecture model is modeled by UPPAAL-SMC model. Each functional prototype corresponds to a time automaton STA model, so the system behavior of the cyber-physical system is represented as a Net-STA model, which is saved in the .xml format as a system model file;

The presentation module is used to formally represent the requirement model of the cyber-physical system CPS in the EAST-ADL architecture model using the probabilistic clock constraint specification language PrCCSL in the editor of the probabilistic clock constraint specification language converter ProTL, and generate the PrCCSL statement;

The construction module is used to describe the grammar of PrCCSL using the BNF language, call the parser generation tool ANTLR, and construct the grammar parser of the PrCCSL language;

The parsing module is used to input the PrCCSL statement into the parser, and parse to generate the abstract syntax tree AST;

The grammar check module is used to check whether the abstract syntax tree AST has any grammar errors. If not, it will enter the generation module. If there is, it will return to the representation module;

The generation module is used to traverse the abstract syntax tree AST to extract the key information of each relationship or expression statement in the PrCCSL statement, and match the corresponding template for each relationship or expression statement according to the content of the key information to generate the STA model and its query statement. Several STA models generate STAs models, save the STAs models as STAs files in .xml format, and generate Query generators for query statements. The generation module includes a mode conversion sub-module for inputting the STAs models into the converter to obtain user Formal verification requirements, if the user verification requirements are obtained, select the PrCCSL+System mode, input the STAs model into the integrator to integrate the system behavior model and the STAs model of the cyber-physical system, and save the output of the integrator in .xml format as Verifiable STAs file; if user authentication requirements are not obtained, select PrCCSL mode and save the STAs model as a STAs file in .xml format;

The integration module is used to input the STAs file into the integrator, integrate the system behavior model of the cyber-physical system, and output a verifiable Net-STA model;

The verification execution module is used to import the verifiable Net-STA model into the verifier, and call the formal verification engine Verifyta of the UPPAAL-SMC model; the Query generator outputs the current query verification statement to Verifyta, and starts Verifyta to perform formal verification.

The above descriptions are only the preferred embodiments of the present invention, and are not intended to limit the scope of the present invention. Under the inventive concept of the present invention, the equivalent structural transformations made by the contents of the description and drawings of the present invention, or the direct/indirect application Other related technical fields are included in the scope of patent protection of the present invention.

Claims (10)

1. doing formalization verification method to network physical system requirements based on UPPAAL-SMC, which is characterized in that including walking as follows It is rapid:

S10 uses probability time constraints specification normative language PrCCSL formalization representation network physical system CPS's in editing machine The demand model of EAST-ADL generates PrCCSL sentence；

PrCCSL input by sentence grammar parser, parsing are generated abstract syntax tree AST by S20；

S30 ergodic abstract syntax tree AST extracts the key message of every relationship or expression statement in PrCCSL sentence, according to pass The content of key information generates STA model and its query statement to every relationship or expression statement matching corresponding template, by several STA model generates STAs model, STAs model is saved as STAs file with .xml format, query statement generates Query and generates Device；

STAs file is inputted integrator by S40, and the system action model of integrated network physical system exports the Net- that can verify that STA model；

The Net-STA model that S50 can verify that imports validator, calls the Formal Verification engine of UPPAAL-SMC model Verifyta,；Query generator exports current queries and verifies sentence to Verifyta, starts Verifyta and executes form chemical examination Card.

2. formalization verification method is done to network physical system requirements based on UPPAAL-SMC as described in claim 1, it is special Sign is that CPS network physical system model includes system architecture model and demand model in the EAST-ADL framework, wherein being System action is indicated with Function Prototypes in system framework model, before the S10 further include:

S01 network physical system is modeled using EAST-ADL framework model, output system framework model and demand model, by UPPAAL-SMC model models the continuous or discrete system action of each Function Prototypes of system architecture model, each Function Prototypes correspond to a Timed Automata STA model, and thus the system action of network physical system is represented as Net-STA mould Type is protected and saves as system model file with .xml format.

3. formalization verification method is done to network physical system requirements based on UPPAAL-SMC as described in claim 1, it is special Sign is, after the S10, before the S20 further include:

S02 uses the grammer of BNF language description PrCCSL, calls resolver Core Generator ANTLR, constructs grammar parser.

4. formalization verification method is done to network physical system requirements based on UPPAAL-SMC as described in claim 1, it is special Sign is, after the S20, before the S30 further include:

S03 checks whether abstract syntax tree AST has syntax error, if not having, enters S30, if so, then returning to S10.

5. formalization verification method is done to network physical system requirements based on UPPAAL-SMC as described in claim 1, it is special Sign is, transformation mode includes PrCCSL mode and PrCCSL+System mode, by STAs model with .xml format in described 30 The step of saving as STAs file include:

S301 is by STAs mode input converter, to obtain user's Formal Verification demand；

If S302 gets user's checking demand, PrCCSL+System mode is selected, by STAs mode input integrator to collect At the system action model of network physical system, the output result of integrator is saved as into the STAs that can verify that using .xml format File；If user's checking demand has not been obtained, PrCCSL mode is selected, STAs model is saved as into STAs text with .xml format Part.

6. formalization verification method is done to network physical system requirements based on UPPAAL-SMC as described in claim 1, it is special Sign is that the content according to key message includes relationship templates to every relationship or the matched corresponding template of expression statement And expression templates.

7. formalization verification method is done to network physical system requirements based on UPPAAL-SMC as described in claim 1, it is special Sign is that the query statement comprises provide that inspection, probability Estimation, emulation, desired value and probability compare five kinds of query statements, institute Query generator is stated including at least above five kinds of query statements and its configuration parameter.

8. formalization verification method is done to network physical system requirements based on UPPAAL-SMC as described in claim 1, it is special Sign is, the demand model of the network physical system CPS includes functional requirement model and non-functional requirement model, described The method of S10 specifically: mutual exclusion, equivalent and sub-clock by the functional requirement of network physical system CPS using PrCCSL language Three kinds of relationships or expression statement indicate；The non-functional requirement of network physical system CPS is used into the preferential of PrCCSL language With represented by two kinds of relationships of cause and effect or expression statement.

9. formalization verification method is done to network physical system requirements based on UPPAAL-SMC as described in claim 1, it is special Sign is, further include S60 in Python call XML DOM to parse .xml file to generate STA model, using Python The library Tkinter at built-in graphical development interface is that every kind of PrCCSL sentence realizes mapping template.

10. one kind makees Formal Verification tool to network physical system requirements based on UPPAAL-SMC characterized by comprising

System modeling module is modeled for network physical system using EAST-ADL framework model, output system framework model and Demand model, by UPPAAL-SMC model to the continuous or discrete system actions of each Function Prototypes of system architecture model into Row modeling, the corresponding Timed Automata STA model of each Function Prototypes, thus the system action of network physical system is expressed For Net-STA model, it is saved as into system model file with .xml format；

Representation module, for using probability time constraints specification normative language PrCCSL formalization representation EAST-ADL in editing machine The demand model of network physical system CPS in framework model generates PrCCSL sentence；

Constructing module calls resolver Core Generator ANTLR, construction for the grammer using BNF language description PrCCSL The grammar parser of PrCCSL language；

Parsing module, for by PrCCSL input by sentence grammar parser, parsing to generate abstract syntax tree AST；

Syntax check module, if not having, enters generation module for checking whether abstract syntax tree AST has syntax error, if Have, then returns to representation module；

Generation module extracts every relationship or the key of expression statement in PrCCSL sentence for ergodic abstract syntax tree AST Information generates STA model and its inquiry to every relationship or expression statement matching corresponding template according to the content of key message Sentence generates STAs model by several STA models, STAs model is saved as STAs file with .xml format, query statement is raw Include that mode converts submodule at Query generator, in the generation module, is used for by STAs mode input converter, to obtain Family Formal Verification demand is taken, if getting user's checking demand, selects PrCCSL+System mode, by STAs model Integrator is inputted with the system action model and STAs model of integrated network physical system, the output result of integrator is used .xml format saves as the STAs file that can verify that；If user's checking demand has not been obtained, PrCCSL mode is selected, by STAs Model saves as STAs file with .xml format；

Module is integrated, for STAs file to be inputted integrator, the system action model of integrated network physical system, output can be tested The Net-STA model of card；

Execution module is verified, the Net-STA model for can verify that imports validator, calls the formalization of UPPAAL-SMC model Validation engine Verifyta,；Query generator exports current queries and verifies sentence to Verifyta, starts Verifyta and executes Formal Verification.