CN109739773B - A GPU Parallel CTL Model Checking Method Based on Pushdown System - Google Patents
A GPU Parallel CTL Model Checking Method Based on Pushdown System Download PDFInfo
- Publication number
- CN109739773B CN109739773B CN201910054917.2A CN201910054917A CN109739773B CN 109739773 B CN109739773 B CN 109739773B CN 201910054917 A CN201910054917 A CN 201910054917A CN 109739773 B CN109739773 B CN 109739773B
- Authority
- CN
- China
- Prior art keywords
- push
- down system
- ctl
- program
- serial
- Prior art date
- Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
- Active
Links
- 238000000034 method Methods 0.000 title claims abstract description 49
- 238000005516 engineering process Methods 0.000 claims abstract description 12
- 238000013508 migration Methods 0.000 claims description 36
- 230000005012 migration Effects 0.000 claims description 36
- 238000012795 verification Methods 0.000 claims description 11
- 238000012546 transfer Methods 0.000 claims description 8
- 210000001151 cytotoxic T lymphocyte Anatomy 0.000 abstract description 54
- 230000006870 function Effects 0.000 abstract description 23
- 238000004458 analytical method Methods 0.000 abstract description 13
- 238000012545 processing Methods 0.000 abstract description 4
- 238000004422 calculation algorithm Methods 0.000 description 5
- 239000003795 chemical substances by application Substances 0.000 description 2
- 238000004590 computer program Methods 0.000 description 2
- 235000014510 cooky Nutrition 0.000 description 2
- 238000013461 design Methods 0.000 description 2
- 238000013459 approach Methods 0.000 description 1
- 230000006399 behavior Effects 0.000 description 1
- 230000009286 beneficial effect Effects 0.000 description 1
- 238000004364 calculation method Methods 0.000 description 1
- 230000001010 compromised effect Effects 0.000 description 1
- 238000011161 development Methods 0.000 description 1
- 238000010586 diagram Methods 0.000 description 1
- 230000000694 effects Effects 0.000 description 1
- 238000007689 inspection Methods 0.000 description 1
- 239000002243 precursor Substances 0.000 description 1
- 238000006467 substitution reaction Methods 0.000 description 1
- 238000012360 testing method Methods 0.000 description 1
- 230000001131 transforming effect Effects 0.000 description 1
Images
Landscapes
- Debugging And Monitoring (AREA)
- Devices For Executing Special Programs (AREA)
Abstract
The invention discloses a method for checking a GPU (graphics processing Unit) parallel CTL (cytotoxic T lymphocyte) model based on a push-down system, which comprises the following steps of: analyzing the serial target program to be verified into a push-down system; generating an alternative Booth-pushing system according to a preset CTL formula and a push-down system; adopting a GPU parallel technology, and solving all received push-down system patterns in the alternative Booth push-down system in parallel through an alternative automaton; and verifying whether the serial target program meets the CTL formula or not according to all the push-down system patterns. The invention automatically constructs a serial JAVA program or a C language program into a push-down system, performs cross multiplication on a CTL formula and the push-down system to generate an alternative Boolean push-down system, dynamically distributes computing tasks by utilizing a GPU parallel technology to adapt to a single-instruction multi-data-stream architecture, and solves all patterns which can be received by an automaton. The method can efficiently carry out null set analysis and CTL model check on the push-down system, and can be used for the analysis of the calling process of the check function and the time sequence property analysis of variable definition.
Description
Technical Field
The invention mainly relates to the technical field of software, in particular to a method for checking a GPU (graphics processing unit) parallel CTL (cytotoxic T lymphocyte) model based on a push-down system.
Background
Reliability and safety of software security have been the focus of attention in the industry. Software bugs can cause national and personal security to be compromised, particularly in the aerospace, industrial control, and rail transit fields. Conventional testing methods do not guarantee the reliability of all possible behaviors of the system. Model checking is a formal method by transforming a program into a formal description and validating the software using graph-theoretic algorithms. The model checking requires a model description program, and the push-down system is a natural serial program formalized model.
The push down system is a limited migration system with stack elements. Because of the property of the push-down system with stack, it can accurately simulate the serial execution procedure and the function calling procedure of the program. In practical applications, the push-down system and its extended model are typically used for analysis and verification of programs. CTL (Computation Tree Logic) is a branch time Logic that can describe the properties of software and is often used for formal verification during software and hardware development. The model checking method based on the push-down system has been a hot point discussed in the industry, and in recent years, a CTL model checking method based on the push-down system executed by symbols has been proposed. This approach converts the problem of pushdown system-based model checking into an empty set analysis problem for an alternative Boolean pushdown system. The algorithm time complexity of the CTL model checking method based on the push-down automaton is reduced from exponential time to polynomial time for the first time. Although this method is more efficient than other CTL model checking algorithms of the same type that have been released in the past, when the verification program becomes complicated and the amount of program code increases, the method still consumes a lot of time and the efficiency is yet to be further improved.
Disclosure of Invention
In order to solve the problems, the invention provides a GPU parallel CTL model checking method based on a push-down system, which automatically constructs a serial JAVA program or a C language program into the push-down system, performs cross multiplication on a CTL formula and the push-down system to generate an alternative Booth push-down system, dynamically distributes computing tasks by utilizing a GPU parallel technology to adapt to a single-instruction multi-data-stream architecture, and solves all patterns which can be received by an automaton.
Specifically, the invention provides a method for checking a GPU parallel CTL model based on a push-down system, which comprises the following steps:
analyzing the serial target program to be verified into a push-down system;
generating an alternative Booth-pushing system according to a preset CTL formula and the push-down system;
adopting a GPU parallel technology to solve all received push-down system patterns in the alternative Booth push-down system in parallel through an alternative automaton;
and verifying whether the serial target program meets the CTL formula or not according to all the push-down system patterns.
Preferably, the parsing the serial object program to be verified into the push-down system includes:
acquiring an entry function of a serial target program to be verified and a transfer parameter of the entry function;
and analyzing the serial object program according to the entry function and the transfer parameter to obtain a push-down system corresponding to the serial object program.
Preferably, the generating the alternative cookie push-down system according to the preset CTL formula and the push-down system includes:
performing standard assignment and regular assignment on the push-down system according to a preset CTL formula;
and performing cross multiplication on the CTL formula and the assigned push-down system to obtain the interchangeable Booth push-down system corresponding to the serial target program.
Preferably, the using a graphics processor GPU parallel technique to solve in parallel, by an interchangeable automaton, a layout of all received pushdown systems in the interchangeable cookie pushdown system comprises:
dividing the alternative automaton into a plurality of independent sub-automatons;
and solving all the push-down system patterns received by the automata in the alternative Booth push-down system in parallel through a GPU thread and the plurality of the sub-automata.
Preferably, the push-down system includes a program control point, a stack element, a program atomic property, and a migration rule, and the method further includes:
determining a pattern code corresponding to each migration rule;
and storing the migration rules included by the push-down system in an index table according to the pattern coding.
Preferably, the storing the migration rule included in the push-down system in an index table according to the pattern coding includes:
storing the migration rules with the same pattern codes in the same table entry in the index table;
determining the number of the migration rules stored in the table entry as a boundary value corresponding to the table entry;
and recording the boundary value corresponding to the table entry in the index table.
Preferably, the solving, in parallel, by the GPU thread and the plurality of sub-automata, the schema of all the pushdown systems received by the automata in the alternative boolean pushdown system includes:
dynamically allocating the plurality of sub-automata to a plurality of GPU computing units;
and acquiring a migration rule from the index table, and expressing the acquired migration rule through a sub-automaton operated in a GPU computing unit to obtain a push-down system pattern received by the sub-automaton.
Further, the method further comprises:
and starting the child threads according to the number of the acquired migration rules through the father thread to perform load balancing.
Further, the method further comprises:
displaying a verification result of CTL formula verification of the serial target program, and displaying all received push-down system configurations.
Further, the method further comprises:
and outputting the final alternative multi-automata, and storing the output alternative multi-automata in a text format file.
Compared with the existing model checking technology, the GPU parallel CTL model checking method based on the push-down system has the following beneficial effects:
the invention automatically constructs a serial JAVA program or a C language program into a push-down system, performs cross multiplication on a CTL formula and the push-down system to generate an alternative Boolean push-down system, dynamically distributes computing tasks by utilizing a GPU parallel technology to adapt to a single-instruction multi-data-stream architecture, and solves all patterns which can be received by an automaton. The method can efficiently carry out null set analysis and CTL model check on the push-down system, and can be used for the analysis of the calling process of the check function and the time sequence property analysis of variable definition.
Drawings
Various other advantages and benefits will become apparent to those of ordinary skill in the art upon reading the following detailed description of the preferred embodiments. The drawings are only for purposes of illustrating the preferred embodiments and are not to be construed as limiting the invention. Also, like reference numerals are used to refer to like parts throughout the drawings. In the drawings:
fig. 1 is a schematic flowchart illustrating a GPU parallel CTL model checking method based on a push-down system according to an embodiment of the present invention.
Fig. 2 is a schematic block diagram illustrating a GPU parallel CTL model checking tool based on a push-down system according to an embodiment of the present invention.
Detailed Description
Exemplary embodiments of the present disclosure will be described in more detail below with reference to the accompanying drawings. While exemplary embodiments of the present disclosure are shown in the drawings, it should be understood that the present disclosure may be embodied in various forms and should not be limited to the embodiments set forth herein. Rather, these embodiments are provided so that this disclosure will be thorough and complete, and will fully convey the scope of the disclosure to those skilled in the art.
Referring to fig. 1, an embodiment of the present invention provides a push-down system-based GPU (Graphics Processing Unit, Graphics processor) parallel CTL model checking method, which specifically includes the following steps:
step 101: and resolving the serial target program to be verified into a push-down system.
The serial object program needs to be a serial program written in C language or JAVA language.
Specifically, an entry function of a serial object program to be verified and a transfer parameter of the entry function are obtained; and analyzing the serial object program according to the entry function and the transfer parameter to obtain a push-down system corresponding to the serial object program. The embodiment of the invention also provides the default assignment attribute of the push-down system according to the serial object program, the push-down system can simulate the calling process of the function, and the default assignment attribute comprises a line number, a variable name, a function name and the like.
The execution subject of the embodiment of the present invention may be a terminal for performing CTL model checking. The entry function of the serial object program and the transfer parameter of the entry function may be input by the user in an input box of the terminal, and the user needs to input the program address of the serial object program in the input box of the terminal. After the terminal acquires the program address, the serial object program can be acquired according to the program address. And then analyzing the serial object program according to the entry function input by the user and the transfer parameter of the entry function, so as to analyze the serial object program into a push-down system.
In an embodiment of the invention, the push-down system includes program control points, stack elements, program atomic properties, and migration rules. Initial values are assigned to each program control point and stack element in the push-down system, including the name of the program control point, the name of the stack, all uses for local variables, all variable definitions, and both definitions and uses for variables. The initial value is composed of characters use, def, usedef, variable name, and method name.
The program atomic property can reflect the calling relationship among functions in the serial object program, and the migration rule is a rule for converting one pattern into another pattern in the push-down system. The schema may be represented by a binary set that includes program control click-to-stack top elements. The above-described entry function is primarily used to determine the initial configuration of the pushdown system.
In the embodiment of the present invention, after the serial object program is parsed into the push-down system, the migration rule included in the push-down system needs to be stored in the index table. Determining the pattern code corresponding to each migration rule; according to the pattern coding, the migration rules included in the push-down system are stored in the index table. Specifically, migration rules with the same pattern code are stored in the same table entry in the index table; determining the number of the migration rules stored in the table entry as a boundary value corresponding to the table entry; and recording the boundary value corresponding to the table entry in the index table.
Step 102: and generating the interchangeable Booth-odd push-down system according to a preset CTL formula and the push-down system.
In the embodiment of the present invention, the preset CTL formula is defined by the user and is input in the input box of the terminal. For example, the CTL formula may be AG (def (x) > EF use (x)), which means that the variable x is used after definition.
Specifically, standard assignment and regular assignment are carried out on the push-down system according to a preset CTL formula; and (4) performing cross multiplication on the CTL formula and the assigned push-down system to obtain the interchangeable Booth push-down system corresponding to the serial target program.
When standard assignments are made to the push-down system, if a schema satisfies that a program atomic property depends only on control points in the schema and not on stack elements, the schema is determined to be the schema of the standard assignments. In the regular assignment of the push-down system, the set of patterns that satisfy a program atomic property is a regular set of patterns.
Step 103: and adopting a GPU parallel technology to solve all received push-down system patterns in the alternative Boolean push-down system in parallel through the alternative automaton.
In the embodiment of the invention, the interchangeable Bucky push-down system is represented by an interchangeable multi-automaton, and all push-down system patterns which can be received by the automaton are solved in parallel by using a GPU parallel technology.
Particularly, the alternative automaton is divided into a plurality of independent sub-automatons; and solving all the push-down system patterns which can be received by the automata in the alternative Boolean push-down system in parallel through the GPU thread and the plurality of sub automata.
Specifically, a plurality of sub automata are dynamically allocated to a plurality of GPU computing units; and acquiring the migration rule from the index table, and expressing the acquired migration rule through a sub-automaton operated in the GPU computing unit to obtain the push-down system pattern received by the sub-automaton.
When the migration rules are obtained from the index table, all the migration rules stored in the table entry are read once according to the boundary value of the table entry. And starting the child threads according to the number of the migration rules through the parent thread to perform load balancing. There is an upper limit to the number of migration rules that each thread can handle. And if the number of the acquired migration rules is larger than the upper limit value, starting the child thread through the father thread to perform load balancing. Specifically, the parent thread calculates a ratio between the number of the acquired migration rules and the upper limit value, performs rounding-up on the ratio, starts integral sub-threads obtained by rounding-up, and obtains all the push-down system patterns which can be received by the automaton by parallelly processing all the acquired migration rules through the started plurality of sub-threads. The embodiment of the invention can dynamically start and close the sub-threads according to the working load of the threads, thereby achieving the effect of load balancing.
Step 104: and verifying whether the serial target program meets the CTL formula or not according to all the push-down system patterns.
And traversing all the push-down system patterns which can be received by the automaton to know whether the serial target program meets the preset CTL formula.
After the CTL verification result of the serial target program is obtained, the verification result of CTL formula verification of the serial target program is displayed, and all the push-down system patterns received by the automaton are displayed, so that a user can conveniently and visually know the model checking result. Further, the final exchangeable multi-automata is also output, and the output exchangeable multi-automata is stored in a text format file.
The method provided by the embodiment of the invention can carry out CTL model check on the serial target program and also support parallel empty set analysis based on the alternative Boolean-Down system. Specifically, the interchangeable Boolean system input by the user is automatically acquired, the interchangeable Boolean system is represented by an interchangeable multi-automaton, all the push-down system patterns which can be received by the automaton are solved in parallel by using a GPU parallel technology, and the empty set analysis is carried out according to all the push-down system patterns which can be received by the automaton.
To facilitate a further understanding of the methods provided by embodiments of the present invention, reference is made to the following brief description taken in connection with the accompanying drawings. As shown in fig. 2, the present invention discloses a push-down system based GPU parallel CTL model checking tool, which includes: the program analysis modeling module is used for analyzing a serial object program (JAVA program or C language program) into a push-down system and giving a default assignment attribute according to the program; the push-down system assignment module is used for performing standard assignment and regular assignment on the push-down system according to the CTL formula and performing cross multiplication on the push-down system and the CTL formula to obtain an alternative Booth push-down system; the parallel CTL model checking module is used for transmitting the interchangeable Boolean system to the initial interchangeable automata, dividing the initial interchangeable automata to obtain a plurality of sub automata, solving all the pushdown system patterns which can be received by the automata in parallel by using a GPU parallel technology through the plurality of sub automata, and traversing all the pushdown system patterns which can be received by the automata to know whether the program meets a CTL formula or not; and the verification result output module is used for displaying and outputting the model checking result of the push-down system and outputting the final alternative multi-automata.
The following describes the method for checking the GPU parallel CTL model based on the push-down system according to the present invention with reference to specific examples. Specifically, the model inspection of the Antlr by applying the method for inspecting the GPU parallel CTL model based on the push-down system of the present invention is taken as an example.
Antlr is an open source parser that can automatically generate a syntax tree from an input and visually display the syntax tree. It is a parser generator based on LL (×) algorithm implementation, written in Java language, using a top-down recursive descent LL parser method. It provides a framework for languages including Java, C + +, C #, to automatically construct recognizers, compilers, and interpreters of custom languages by syntactic descriptions.
In this example, the defined calling order of a certain variable is verified. The specific operation steps are as follows:
step a, first, a CTL formula is determined, for example, the CTL formula AG (def (x) - > EF use (x)) indicates that the variable x is definitely used after being defined.
And step B, inputting the program address of the verified target program, the main function inlet of the verified target program and the CTL formula into the terminal input box.
And step C, modeling the verified target program into a push-down system by the program analysis modeling module. From the target source code, the program is modeled as a push-down system that includes program control points, stack elements, program atomic properties, and migration rules.
For example, a function call may be regarded as pushing a new stack element in the program stack, and the function call ends to pop up the top element of the program stack. And gives the nature of the push down system and gives the default assignments.
Step D, inputting the push-down system into a push-down system assignment module, performing standard assignment on the push-down system according to a CTL (program control language) formula, and performing cross multiplication on the push-down system and the CTL formula to obtain an alternative Booth push-down system;
and step E, representing the alternative Boolean system by an alternative multi-automaton, wherein the initial automaton receives all the patterns. The automaton is divided into a plurality of irrelevant sub automatons which are calculated in a GPU thread in parallel. And the thread judges the thread load according to the boundary value of the table items in the parallel index table, and the sub-thread shares tasks when the load is overlarge, so that load balance is realized.
And F, after the precursor search of the automaton is completed, the GPU task returns to the CPU. And judging whether the automaton reaches the fixed point or not. If the motionless point has been reached, the calculation ends. And if the fixed point is not reached, the task returns to the GPU for next loop iteration.
And G, displaying and outputting the model checking result of the push-down system in a terminal display window, and outputting the final alternative multi-automata, wherein the output result file is stored in a text form.
In the embodiment of the invention, a serial JAVA program or a C language program can be automatically constructed into a push-down system, and the basic attribute assignment is given according to the code line number, the variable name and the function name. According to the design requirement of a program system, the property needing safety verification is manually extracted and expressed as a CTL formula. The tool automatically performs cross multiplication on the CTL formula and the push-down system to generate an interchangeable Boolean push-down system, dynamically distributes computing tasks by using a GPU parallel technology to adapt to a single-instruction multi-data-stream architecture, and solves all patterns which can be received by the interchangeable Boolean push-down system. The method can efficiently carry out null set analysis and CTL model check on the push-down system, and can be used for the analysis of the calling process of the check function and the time sequence property analysis of variable definition.
It should be noted that:
the algorithms and displays presented herein are not inherently related to any particular computer, virtual machine, or other apparatus. Various general purpose devices may be used with the teachings herein. The required structure for constructing such a device will be apparent from the description above. Moreover, the present invention is not directed to any particular programming language. It is appreciated that a variety of programming languages may be used to implement the teachings of the present invention as described herein, and any descriptions of specific languages are provided above to disclose the best mode of the invention.
In the description provided herein, numerous specific details are set forth. It is 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 should be appreciated that in the foregoing description of exemplary embodiments of the invention, various features of the invention are sometimes grouped together in a single embodiment, figure, or description thereof for the purpose of streamlining the disclosure and aiding in the understanding of one or more of the various inventive aspects. However, the disclosed system should not be interpreted to reflect the intent: 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 of the embodiments may be adaptively changed and disposed in one or more devices other than the embodiments. Steps or components in the embodiments may be combined into one step or component, and further, may be divided into a plurality of steps or sub-components. All of the features disclosed in this specification (including any accompanying claims, abstract and drawings), and all of the processes or steps of any system or apparatus so disclosed, may be combined in any combination, except combinations where at least some of such features and/or processes or steps are mutually exclusive. Each feature disclosed in this specification (including any 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 while some embodiments described herein include some features included in other embodiments, rather than other features, combinations of features of different embodiments are meant to be within the scope of the invention and form different embodiments. For example, in the following claims, any of the claimed embodiments may be used in any combination.
The various component embodiments of the 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 will appreciate that a microprocessor or Digital Signal Processor (DSP) may be used in practice to implement some or all of the functions of some or all of the components in the creation apparatus of a virtual machine according to embodiments of the present invention. The present invention may also be embodied as apparatus or device programs (e.g., computer programs and computer program products) for performing a portion or all of the system described herein. Such programs implementing the present invention may be stored on computer-readable media or may be in the form of one or more signals. Such a signal may be downloaded from an internet website or provided on a carrier signal or in any other form.
It should be noted that the above-mentioned embodiments illustrate rather than limit the invention, and that those skilled in the art will be able to design alternative embodiments 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 may be implemented by means of hardware comprising several distinct elements, and by means of a suitably programmed computer. In the step claims enumerating several means, several of these means may be embodied by one and the same item of hardware. The usage of the words first, second and third, etcetera do not indicate any ordering. These words may be interpreted as names.
The above description is only for the preferred embodiment of the present invention, but the scope of the present invention is not limited thereto, and any changes or substitutions that can be easily conceived by those skilled in the art within the technical scope of the present invention are included in the scope of the present invention. Therefore, the protection scope of the present invention shall be subject to the protection scope of the appended claims.
Claims (8)
Priority Applications (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN201910054917.2A CN109739773B (en) | 2019-01-21 | 2019-01-21 | A GPU Parallel CTL Model Checking Method Based on Pushdown System |
Applications Claiming Priority (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN201910054917.2A CN109739773B (en) | 2019-01-21 | 2019-01-21 | A GPU Parallel CTL Model Checking Method Based on Pushdown System |
Publications (2)
| Publication Number | Publication Date |
|---|---|
| CN109739773A CN109739773A (en) | 2019-05-10 |
| CN109739773B true CN109739773B (en) | 2021-01-29 |
Family
ID=66365481
Family Applications (1)
| Application Number | Title | Priority Date | Filing Date |
|---|---|---|---|
| CN201910054917.2A Active CN109739773B (en) | 2019-01-21 | 2019-01-21 | A GPU Parallel CTL Model Checking Method Based on Pushdown System |
Country Status (1)
| Country | Link |
|---|---|
| CN (1) | CN109739773B (en) |
Families Citing this family (1)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| CN109814928B (en) * | 2019-01-21 | 2021-01-29 | 华东师范大学 | GPU parallel CTL model checking system based on push-down system |
Citations (4)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US8136098B2 (en) * | 2006-07-12 | 2012-03-13 | Nec Laboratories America, Inc. | Using pushdown systems for the static analysis of multi-threaded programs |
| CN102929781A (en) * | 2012-11-12 | 2013-02-13 | 桂林电子科技大学 | Queue communication concurrency recursive program verification method based on context delimiting |
| CN104267936A (en) * | 2014-09-16 | 2015-01-07 | 桂林电子科技大学 | Semantic tree based asynchronous dynamic push-down network reachability analysis method |
| CN106940659A (en) * | 2017-03-09 | 2017-07-11 | 华东师范大学 | Interruption verification method based on the lower pushing system of weighting |
Family Cites Families (6)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US8266600B2 (en) * | 2005-03-28 | 2012-09-11 | Nec Laboratories America, Inc. | Model checking of multi threaded software |
| CN101695079A (en) * | 2009-09-30 | 2010-04-14 | 北京航空航天大学 | Automatic service combination method capable of guaranteeing correction and system thereof |
| US8296735B2 (en) * | 2010-02-19 | 2012-10-23 | National Ict Australia Limited | Inter-procedural analysis of computer programs |
| CN107016524A (en) * | 2015-12-18 | 2017-08-04 | Sap欧洲公司 | Steered reference process extensibility framework |
| CN106446341A (en) * | 2016-08-29 | 2017-02-22 | 华东师范大学 | Process algebra-based real-time protocol analysis and verification system |
| CN109814928B (en) * | 2019-01-21 | 2021-01-29 | 华东师范大学 | GPU parallel CTL model checking system based on push-down system |
-
2019
- 2019-01-21 CN CN201910054917.2A patent/CN109739773B/en active Active
Patent Citations (4)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US8136098B2 (en) * | 2006-07-12 | 2012-03-13 | Nec Laboratories America, Inc. | Using pushdown systems for the static analysis of multi-threaded programs |
| CN102929781A (en) * | 2012-11-12 | 2013-02-13 | 桂林电子科技大学 | Queue communication concurrency recursive program verification method based on context delimiting |
| CN104267936A (en) * | 2014-09-16 | 2015-01-07 | 桂林电子科技大学 | Semantic tree based asynchronous dynamic push-down network reachability analysis method |
| CN106940659A (en) * | 2017-03-09 | 2017-07-11 | 华东师范大学 | Interruption verification method based on the lower pushing system of weighting |
Non-Patent Citations (1)
| Title |
|---|
| Model checking CTL Properties of Pushdown;Igor Walukiewicz;《Conference on Foundations of Software Technology & Theoretical Computer Science》;20001213;1-12 * |
Also Published As
| Publication number | Publication date |
|---|---|
| CN109739773A (en) | 2019-05-10 |
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| EP3631618B1 (en) | Automated dependency analyzer for heterogeneously programmed data processing system | |
| Richters et al. | Validating UML models and OCL constraints | |
| Di Ciccio et al. | Generating event logs through the simulation of declare models | |
| US9207935B2 (en) | Early analysis of software design diagrams | |
| WO2019075390A1 (en) | Blackbox matching engine | |
| US8943003B2 (en) | Composite production rules | |
| US12182732B2 (en) | Automated decision platform | |
| WO2012032890A1 (en) | Source code conversion method and source code conversion program | |
| TWI826702B (en) | Techniques for defining and executing program code specifying neural network architectures | |
| CN107797805B (en) | Code packaging method and device and computer readable storage medium | |
| US20150378977A1 (en) | System and method for operating a computer application with spreadsheet functionality | |
| JPWO2017159638A1 (en) | Capability grant data generator | |
| US20100275183A1 (en) | Source code auditor with a customized rules builder | |
| CN116578475A (en) | A code verification method, device, equipment and readable storage medium | |
| CN109739773B (en) | A GPU Parallel CTL Model Checking Method Based on Pushdown System | |
| CN109814928B (en) | GPU parallel CTL model checking system based on push-down system | |
| CN108563561A (en) | A kind of program recessiveness constraint extracting method and system | |
| CN110928535A (en) | Derivative variable deployment method, device, equipment and readable storage medium | |
| Blazy et al. | Verified validation of program slicing | |
| CN119759356A (en) | Code generation method, device and electronic device based on large model | |
| CN114691111A (en) | Code recognition model training method and device based on visualization | |
| CN114327753A (en) | Method, device, equipment and medium for predicting container construction results | |
| CN114489774B (en) | Web application packaging method, device, equipment and storage medium | |
| Ajila et al. | Aspectualization of code clones—an algorithmic approach | |
| CN116069633B (en) | Code inspection methods, devices, electronic equipment and storage media |
Legal Events
| Date | Code | Title | Description |
|---|---|---|---|
| PB01 | Publication | ||
| PB01 | Publication | ||
| SE01 | Entry into force of request for substantive examination | ||
| SE01 | Entry into force of request for substantive examination | ||
| GR01 | Patent grant | ||
| GR01 | Patent grant | ||
| TR01 | Transfer of patent right | ||
| TR01 | Transfer of patent right |
Effective date of registration: 20210806 Address after: Room 801, no.6, Lane 600, Yunling West Road, Putuo District, Shanghai 200062 Patentee after: SHANGHAI FORMAL TECH INFORMATION TECHNOLOGY Co.,Ltd. Address before: 200062 No. 3663, Putuo District, Shanghai, Zhongshan North Road Patentee before: EAST CHINA NORMAL University Patentee before: SHANGHAI FORMAL TECH INFORMATION TECHNOLOGY Co.,Ltd. |