JP4905173B2 - Software verification apparatus, software verification method, and software verification program - Google Patents

Description

  The present invention relates to a software verification apparatus, a software verification method, and a software verification program for verifying software that can be divided into a plurality of modules.

  When verifying the correctness of the operation of a large-scale software, as a method of verifying the whole from partial verification, the theory proposed by Hoare (Hoer theory) (see Non-Patent Document 1) and Meyer Programming based on a proposed contract (see Non-Patent Document 2) is known.

  According to the rules of compound statements in Hoer theory, a program is divided into a plurality of partial programs, and the conditions to be satisfied among the divided partial programs (the post-conditions of the previously processed partial program and the next processing) Given the preconditions of the partial program to be executed, the original program can be verified by verifying the partial program based on these conditions. Further, according to programming by contract, it is possible to verify that the entire program operates properly by giving pre-conditions and post-conditions of routines constituting the program as assertions. In any case, the entire program can be verified by dividing the program into appropriate parts and appropriately giving pre-processing and post-processing conditions to the divided parts.

By Hayashi Hayashi, “Program Verification Theory”, Kyoritsu Shuppan, September 1, 1995, pp. 28 By Bertrand Meyer, translated by Akiyoshi Futaki, "Introduction to Object Orientation", ASCII Publishing, November 21, 1990, pp. 153-168

  In the methods described in Non-Patent Documents 1 and 2, the verification operator divides the target software into a plurality of modules and is a condition that is to be satisfied among the modules having a call relationship (the caller's post-condition and called) Side precondition). Under the conditions, the divided individual modules are individually verified one after another, and the verification result of all the modules is obtained to verify the entire target software. In this case, the verification worker performs verification by dividing into several modules in advance so that the verification does not exceed the memory capacity of the system and the verification is completed within an allowable time. The range to be defined and the conditions to be satisfied between the calling modules must be set appropriately.

  Therefore, the present invention provides a software verification apparatus, a software verification method, and a software verification program capable of performing software verification without specifying a partial verification range and setting conditions to be satisfied between modules having a calling relationship. The purpose is to do.

A software verification apparatus according to the present invention is a software verification apparatus that verifies software that can be divided into a plurality of modules. The module constituting the software is a verification target, and the verification target module has a predetermined verification item without a precondition. When the determination means (for example, the central processing unit 111) for determining whether or not the verification item is satisfied and the determination means determine that the verification item may not be satisfied, the verification item at the start of the verification target module does not hold. The condition calculation means (for example, the central processing unit 111) for calculating the condition of the process and the processing result from the highest module in the calling relationship between modules to the start time of the module to be verified are the conditions calculated by the condition calculation means. Condition determining means for determining whether or not it is satisfied (for example, central processing unit) 11) and, based on the determination of the condition determination means, it is determined whether or not the verification item is satisfied for the verification target module. When the condition determination unit determines that the condition is not satisfied, the verification item is verified for the verification target module. And a module determination unit (for example, central processing unit 111) that determines that the predetermined verification items for the software are satisfied based on the determination by the module determination unit. 111), and when the module determination unit determines that the verification item does not hold for the verification target module because the condition determination unit determines that the condition calculated by the condition calculation unit is satisfied , Determining that certain verification items do not hold for software And butterflies.

  When it is impossible to determine whether the verification item is valid for the verification target module, the determination means sequentially sets the lower module that may call the module including the verification item as the verification target, without any preconditions. If the determination means or the module determination means determines that the verification items are satisfied for all the lower modules, the module determination unit recursively if the verification items are satisfied for the upper verification target module. It is desirable to make a judgment. According to such a configuration, verification can be performed accurately and efficiently.

  The determination means determines whether or not the verification item is valid with respect to the highest module in the calling relationship between the modules, and the software determination means is that the determination means or the module determination unit satisfies the verification item for all the lower modules. It is desirable to determine that the verification items hold for the entire software. According to such a configuration, the entire software can be verified.

  The software verification device includes an output device (for example, the output device 112) that outputs the verification result or a storage device (for example, the secondary storage device 114) that stores the verification result, and the software determination unit outputs the determined result to the output device. Or you may output to a memory | storage device. According to such a configuration, the verification result can be output or stored.

The software verification method according to the present invention is a software verification method for verifying software that can be divided into a plurality of modules. The module constituting the software is a verification target, and the verification target module has a predetermined verification item without a precondition. A determination step for determining whether or not the condition is satisfied, and a condition calculation step for calculating a condition for not verifying the verification item at the start of the verification target module when it is determined that the verification item may not be satisfied in the determination step. And a condition determination step for determining whether or not the condition calculated in the condition calculation step is satisfied in the processing result from the highest module in the calling relationship between the modules to the start time of the module to be verified. Based on the determination of In the module determination step and the module determination step, it is determined whether the verification items are satisfied for the verification target module when it is determined that the conditions are not satisfied in the condition determination step. And a software determination step for determining whether or not a predetermined verification item is satisfied for the software, and in the software determination step, the condition determination step determines that the condition calculated in the condition calculation step is satisfied , When it is determined in the module determination step that the verification item does not hold for the verification target module, it is determined that the predetermined verification item does not hold for the software.

A software verification program according to the present invention is a software verification program for verifying software that can be divided into a plurality of modules, and the module constituting the software is targeted for verification in a computer without any preconditions. The determination process for determining whether or not a predetermined verification item is satisfied, and the conditions for not verifying the verification item at the start of the module to be verified when it is determined that the verification process may not be satisfied in the determination process. A condition calculation process for calculating, and a condition determination process for determining whether or not the condition calculated in the condition calculation process is satisfied in the processing result from the highest module in the calling relationship between modules to the start time of the verification target module; Based on the determination in the condition determination process, The module determination process for determining whether the verification items are satisfied for the module to be verified, and the determination in the module determination processing when it is determined whether the verification items are satisfied for the rule and the condition determination processing determines that the conditions are not satisfied based on that, to execute a determining software determination process whether or not a predetermined verification item holds the software, the software determination process, it is determined by the condition determination processing and condition calculated by the condition calculating process is satisfied Thus, when it is determined in the module determination process that the verification item does not hold for the verification target module, it is determined that the predetermined verification item does not hold for the software.

  According to the present invention, the operator sets the precondition when dividing and verifying in order to obtain the precondition when the verification item does not hold and to check whether the precondition is satisfied from the top module. There is an effect that the software can be easily verified. In addition, verification is performed recursively from the top module, and only when it is determined that the verification item does not hold, the condition for the verification item not being calculated is obtained. There is an effect that verification can be performed.

  Hereinafter, embodiments of the present invention will be described with reference to the drawings. FIG. 1 is a block diagram showing a configuration example of a software verification apparatus according to the present invention. The software verification device shown in FIG. 1 includes a central processing unit 111, an output device 112, a primary storage device 113, and a secondary storage device 114.

  The central processing unit 111 reads the source code of the verification target software stored in the secondary storage device 114, performs verification processing, and outputs the verification result to the output device 112.

  The output device 112 is a display device, a printing device, or the like. The primary storage device 113 stores various data such as a verification program for the software verification device to perform verification and data temporarily required for the central processing unit 111 to execute the program. The secondary storage device 114 stores the source code of the verification target software.

  The verification function described below is implemented as a part of the central processing unit 111 shown in FIG. When the software verification apparatus is realized by a computer, the central processing unit 111 is realized by executing a program for realizing a verification function described below.

  FIG. 2 is an explanatory diagram illustrating an example of a module structure of the verification target software. m1 to m7 are modules. Arrows indicate call relationships between modules. Moreover, p shows the property (verification matter) which should be verified. In the example shown in FIG. 2, the property to be verified is a condition that should be observed at a certain location of the module m7. A portion surrounded by a broken line is a verification range Mi starting from the module mi (i = 1, 2, 3, 6).

  A verification method according to the present embodiment will be described with reference to FIG. In order to verify whether the property p is protected in the entire software, first, verification is performed from the highest module m1. If it is not possible to determine whether or not the property p is protected in the verified module, whether or not the property p is protected for the lower modules m2 and m3 that may call the module m7 including p. The module m1 is recursively verified by verifying without a precondition until the determination result is obtained.

  If a determination result that the property p is not observed is obtained for any of the lower modules, a condition for preventing the property is obtained as a precondition at the start of verification in the lower module. Then, the property p is verified in order from the highest module to the lower module without a precondition, and it is determined whether or not a condition for preventing the property from being satisfied at the start of verification of the lower module. Suppose that the property is not protected even in the whole software when the condition for not being protected is satisfied. In addition, when it is determined that the property p is protected for all the lower modules, the property is also protected for the entire software.

  Next, the operation of the present embodiment will be described with reference to the drawings. FIG. 3 is a flowchart showing the verification processing in the present embodiment. Hereinafter, a case where the central processing unit 111 performs the property p verification process will be described.

  First, the central processing unit 111 sets the highest module as the verification starting module ms (step S1). The central processing unit 111 verifies from the start point module ms whether the property p is protected without a precondition (step S2).

  In step S3, the central processing unit 111 determines whether or not the property p is protected. In step S3, when it is impossible to determine whether or not the property p is observed, the central processing unit 111 is a module that may call a module including p among modules called directly from the origin module ms (a module including p). A set Mc (including itself) is generated (step S9). In step S10, the central processing unit 111 determines whether or not Mc is an empty set. If Mc is an empty set (YES), the verification result Rs of ms is set to “determination impossible” (step S11). If Mc is not an empty set (NO), each module included in the set Mc is set as the starting module ms, and the process from step S2 is recursively repeated (step S12), and the subsequent determination is performed.

  If the central processing unit 111 determines in step S3 that the property p is protected in the starting module ms (YES), the verification result Rs of ms is determined as “property p is protected” (step S4), and the process proceeds to step S18. To do.

  If the central processing unit 111 determines in step S3 that the property p is not observed (NO), the central processing unit 111 obtains a condition for preventing the property p from being satisfied as the condition Cf at the start of verification in the starting module ms (step S3). S5).

  The central processing unit 111 sets a module group on the path that traces the calling relationship in the reverse direction from the module ms to the highest module as the verification range Mu. In the verification range Mu, the central processing unit 111 verifies the property p without any preconditions starting from the highest module, and verifies whether the condition Cf is satisfied when ms is called (step S6). That is, the central processing unit 111 verifies whether or not the condition Cf is satisfied in the processing results from the highest module in the calling relationship between modules to the start time of the verification target module.

  In step S7, the central processing unit 111 determines whether or not the condition Cf is satisfied when ms is called, and if it is determined that it is satisfied (YES), the verification result Rs of ms is “the property p is not protected”. (Step S8), the process proceeds to Step S18.

  When it is determined in step S7 that the condition Cf does not hold (NO), the central processing unit 111 sets the ms verification result Rs to “property p is protected” (step S4), and proceeds to step S18. When the determination is impossible, the central processing unit 111 sets the ms verification result Rs to “determination impossible” (step S11), and proceeds to step S18. In step S18, it is determined whether ms is the highest module. If ms is not the highest module (NO), the process returns to step S12 (step S19).

  When the central processing unit 111 has calculated the verification results for all the modules of the set Mc, the central processing unit 111 proceeds to step S13. In step S13, the central processing unit 111 determines whether or not the property p is protected for all modules in Mc. When it is determined that the property p is protected for all modules in Mc (YES), the central processing unit 111 sets the ms verification result Rs to “property p can be protected” (step S14), and the process proceeds to step S18. Transition.

If it is determined in step S13 that the property p is not protected for all the modules in Mc (NO), the central processing unit 111 determines in step S15 that there is a module in which the property p is not protected in Mc. It is determined whether or not there is. When the central processing unit 111 determines that there is a module in which the property p is not protected in Mc (YES), the central processing unit 111 sets the ms verification result Rs to “property p is not protected” (step S16), and proceeds to step S18. Transition. If none of them, that is, if there is no module whose property p is not protected in Mc and any module cannot be determined (NO), the ms verification result Rs is set to “determination impossible” (step S17). The process proceeds to step S18.

  In step S18, the central processing unit 111 determines whether ms is the highest module. If ms is not the highest module (NO), the process returns to step S12 (step S19). On the other hand, if ms is the highest module (YES), the verification result Rs of ms is set as the verification result R of the property p of the entire software (step S20), and the series of processing is terminated.

  Further, the central processing unit 111 outputs, for example, the verification result of each module and the verification result of the entire software to the output device 112.

  Next, a specific example of the operation of the present embodiment will be described with reference to FIGS. Hereinafter, the module structure of the verification target software shown in FIG. 2 will be described as an example. FIG. 4 is an explanatory diagram illustrating an example of processing contents of the verification target software. In FIG. 4, it is assumed that processing contents are described in a C language style, and each module shown in FIG. 2 corresponds to the function of the same name shown in FIG. Further, the property p to be verified is “do not perform memory access beyond the upper limit of the array in the process of a [idx] = − 1 in the module m7”. Further, it is assumed that the property p cannot be verified (cannot be determined) in the modules m1, m2, and m3 due to resource constraints.

  m1 is set as the verification starting module ms (step S1), and it is verified from the starting module ms whether the property p is protected without a precondition (step S2). In step S3, since the verification result cannot be determined, Mc = {m2, m3} is generated as a set of modules that may call m7 including p among modules called directly from ms (= m1) ( Step S9). FIG. 5 is an explanatory diagram showing an example of the verification range M1 when ms = m1 and a set Mc = {m2, m3} of modules called from m1 and calling a module including p. In Step S10, since Mc is not an empty set (NO), the processing from Step S2 is recursively repeated for the elements m2 and m3 of Mc (Step S12).

  m2 is set as the starting module ms (step S1), and it is verified from the starting module ms whether the property p is protected without a precondition (step S2). Since the verification result cannot be determined in step S3, the central processing unit 111 generates a set Mc (step S9). Here, only m6 that has a possibility of calling m7 out of modules called directly from m2 is an element of the next Mc. FIG. 6 is an explanatory diagram showing an example of the verification range M2 when ms = m2 and a set Mc = m6 of modules called from m2 and calling module m7 including p. The process from step S2 is repeated for ms = m6.

  The starting point module ms is set starting from m6 (step S1), and it is verified from the starting point module ms whether the property p is protected without a precondition (step S2). In step S3, the central processing unit 111 determines that the property p is not necessarily protected (NO). The central processing unit 111 calculates a condition Cf for preventing the property p from being observed at the time of starting verification of ms (= m6) as idx ≧ 2 (step S5). FIG. 7 is an explanatory diagram illustrating an example of the verification range M6 when ms = m6 and the verification range Mu = {m1, m2} for verifying the condition Cf from the highest module.

  The central processing unit 111 verifies whether or not the condition Cf is satisfied, using the uppermost module m1 and Mu = {m1, m2} as a verification range without a precondition (step S6). When m6 is called, idx = 1 and Cf is not established (NO in step S7), so the verification result Rs of ms (= m6) is “property p is protected” (step S4).

  Since ms (= m6) at this time is not the highest module m1, the process proceeds to step S2 (step S19). Since the verification result is calculated for the set Mc = m6, the process proceeds to step S13, and the verification result of m2 is obtained from the verification result of the lower module group Mc of m2. Here, the module included in Mc is only m6, and the verification result of m6 is “property p is protected”. Therefore, the verification result of all lower modules of m2 is “property p is protected” (YES in step S13), and the verification result Rs of ms (= m2) is “property p is protected” (step S14). In step S18, ms (= m2) is not the highest module m1, so the process proceeds to step S12 (step S19).

  Next, m3 is set as the starting module ms (step S1), and it is verified from the starting module ms whether the property p is protected without a precondition (step S2). In step S3, since the verification result of m3 cannot be determined, the central processing unit 111 generates a set Mc (step S9). In step S9, the central processing unit 111 generates Mc having only the module m7 that is directly called from m3 as an element. FIG. 8 is an explanatory diagram showing an example of the verification range M3 when ms = m3 and a set Mc = m7 of modules called from m3 and including p. For ms = m7, the process from step S2 is repeated.

  m7 is set as the starting module ms (step S1), and it is verified whether the property p is protected without a precondition (step S2). In step S3, the central processing unit 111 determines that the property p is not necessarily protected (NO). The central processing unit 111 calculates, as idx ≧ 4, a condition Cf for not observing the property p at the time of starting verification of ms (= m7) (step S5).

  FIG. 9 is an explanatory diagram illustrating an example of the verification range M7 when ms = m7 and the verification range Mu = {m1, m3} for verifying the condition Cf from the highest module.

  The central processing unit 111 verifies whether or not the condition Cf is satisfied, using the highest module m1 to Mu = {m1, m3} as a verification range without a precondition (step S6). When m7 is called, idx = 4 and Cf is established (YES in step S7), and the verification result Rs of ms (= m7) is “property p is not protected” (step S8).

  Since ms (= m7) at this time is not the highest module m1, the process proceeds to step S2 (step S19). Since the verification result is calculated for the set Mc = m7, the process proceeds to step S13, and the verification result of m3 is obtained from the verification result of the lower module group Mc of m3. Here, since there is an element m7 in Mc that “property p is not protected” (YES in step S15), the verification result Rs of ms (= m3) is “property p is not protected” (step S16). . In step S18, ms (= m3) is not the highest module m1, so the process proceeds to step S12 (step S19).

  Since all the verification results of the lower module group Mc = {m2, m3} of ms (= m1) are calculated, the process proceeds to step S13, and the verification of m1 is verified from the verification result of the lower module group Mc = {m2, m3} of m1. Find the result.

  Since there is an element m3 that “property p is not protected” in Mc (YES in step S15), the verification result Rs of ms (= m1) becomes “property p is not protected” (step S16). Since ms (= m1) is the highest module m1, the verification result Rs of ms (= m1) is set as the verification result R of the property p of the entire software, and “property p is not protected” (step S20). Exit.

  As described above, according to the present embodiment, partial verification is performed to obtain a precondition when the property p is not observed, and whether or not the precondition is satisfied from the highest module is confirmed. Therefore, it is possible to omit the setting work of the condition to be satisfied between the modules having the calling relationship, and the software can be easily verified as compared with the case where the operator sets the precondition when the divided verification is performed. Can do.

  In addition, recursive verification is performed from the top module, and only when a verification result is obtained, a condition is obtained based on the result, so inappropriate condition setting can be avoided, and software verification can be performed accurately. It can be performed.

  Furthermore, based on the calling relationship of the modules that make up the software, the verification starting point is recursively verified from the highest module while changing the calling origin from the higher module to the lower module. Verify by lowering the module. That is, when the verification result of the verification target module becomes indeterminate, the lower module is verified, and the process of obtaining the verification result of the upper module from the verification result of the lower module is recursively repeated. Therefore, large-scale software can be properly divided to verify specific characteristics, and verification work can be omitted accurately because the verification work performed by the verification operator manually can be omitted. be able to.

  For example, only when the verification result of the verification target module becomes indeterminate, the verification is performed by lowering the module (that is, partial verification), so verification in a large context is possible, and in a small context The verification can be performed more accurately than when verification is repeated (an error may occur each time). In addition, since only necessary portions are divided and verified, overhead due to the division can be reduced, so that verification can be performed efficiently.

  In the above embodiment, the central processing unit 111 outputs the verification result of each module and the verification result of the entire software to the output device 112 as an example, but the output device 112 may not be provided. In that case, the central processing unit 111 may output the final processing result to the secondary storage device 114, for example.

  The present invention can be effectively applied to verifying software including a plurality of modules having a calling relationship.

It is a block diagram which shows the structural example of the software verification apparatus by this invention. It is explanatory drawing which shows the example of the module structure of verification object software. It is a flowchart which shows a verification process. It is explanatory drawing which shows the example of the processing content of verification object software. It is explanatory drawing which shows the example of the verification range and the set Mc of a module. It is explanatory drawing which shows the example of the verification range and the set Mc of a module. It is explanatory drawing which shows the example of the verification range and the verification range Mu. It is explanatory drawing which shows the example of the verification range and the set Mc of a module. It is explanatory drawing which shows the example of the verification range and the verification range Mu.

Explanation of symbols

111 Central Processing Unit 112 Output Unit 113 Primary Storage Unit 114 Secondary Storage Unit

Claims (6)

A software verification device for verifying software that can be divided into a plurality of modules,
A determination unit that determines whether or not a predetermined verification item is satisfied without a precondition for a verification target module, with a module constituting the software as a verification target;
Condition determining means for calculating a condition for not verifying the verification items at the start of the verification target module when the determination unit determines that the verification items may not be satisfied; and
Condition determination means for determining whether the condition calculated by the condition calculation means is satisfied in the processing result from the highest module in the calling relationship between modules to the start time of the module to be verified;
Based on the determination of the condition determination means, it is determined whether or not a verification item is satisfied for the verification target module, and when the condition determination unit determines that the condition is not satisfied, a verification item for the verification target module is determined. Module determination means for determining that
Software determination means for determining whether or not a predetermined verification item holds for the software based on the determination of the module determination means ;
The software determination means determines that the condition determination means determines that the condition calculated by the condition calculation means is satisfied, so that the module determination means determines that the verification item does not hold for the verification target module. A software verification device that determines that a predetermined verification item does not hold for software. When it is impossible to determine whether the verification item is valid for the verification target module, the determination means sequentially sets the lower module that may call the module including the verification item as the verification target, without any preconditions. Determine whether or not
The module determination unit recursively determines that the verification item holds for the higher verification target module when the determination unit or the module determination unit determines that the verification item holds for all the lower modules. Software verification equipment. The determination means determines whether or not the verification item is satisfied with the highest module in the calling relationship between modules as the verification target,
The software verification apparatus according to claim 2, wherein the software determination unit determines that the verification item holds for the entire software when the determination unit or the module determination unit determines that the verification item holds for all the lower modules. The software verification device includes an output device that outputs a verification result or a storage device that stores the verification result,
The software verification device according to any one of claims 1 to 3, wherein the software determination unit outputs the determined result to the output device or the storage device. A software verification method for verifying software that can be divided into a plurality of modules,
A determination step for determining whether or not a predetermined verification item is satisfied without a precondition for a verification target module with a module constituting the software as a verification target;
A condition calculating step for calculating a condition for not satisfying the verification item at the start of the verification target module when it is determined that the verification item may not be satisfied in the determination step;
A condition determination step for determining whether or not the condition calculated in the condition calculation step is satisfied in the processing result from the highest module in the calling relationship between modules to the start time of the verification target module;
Based on the determination in the condition determination step, it is determined whether verification items are satisfied for the verification target module, and if it is determined that the condition is not satisfied in the condition determination step, the verification target module is verified. A module determination step for determining that the matter is satisfied;
A software determination step for determining whether or not a predetermined verification item holds for the software based on the determination in the module determination step,
In the software determination step, when it is determined in the module determination step that the verification item does not hold because the condition determination step determines that the condition calculated in the condition calculation step is satisfied. And determining that a predetermined verification item does not hold for the software. A software verification program for verifying software that can be divided into a plurality of modules,
On the computer,
A determination process for determining whether or not a predetermined verification item is satisfied without a precondition for a verification target module with a module constituting the software as a verification target;
A condition calculation process for calculating a condition for not verifying at the start of the verification target module when it is determined that the verification process may not be satisfied in the determination process;
Condition determination processing for determining whether or not the condition calculated in the condition calculation processing is satisfied in the processing result from the highest module in the calling relationship between modules to the start time of the verification target module;
Based on the determination in the condition determination process, it is determined whether verification items are satisfied for the verification target module, and if it is determined that the condition is not satisfied in the condition determination process, the verification target module is verified. A module determination process for determining that the matter is satisfied;
Based on the determination in the module determination process, to execute a software determination process to determine whether or not a predetermined verification item holds for the software,
In the software determination process, when it is determined in the module determination process that the condition calculated in the condition calculation process is satisfied, it is determined in the module determination process that verification items do not hold for the verification target module And a software verification program for determining that a predetermined verification item does not hold for the software.

Images