JP5643971B2 - Source code conversion method and source code conversion program - Google Patents

Description

  The present invention relates to a source code conversion method and a source code conversion program, and in particular, in a software model check, in order to reduce the cost of writing a check code in an input language of a model checker, a software source is utilized by utilizing a computer. The present invention relates to a method for converting a code into an inspection code.

  In recent years, software systems have spread to the general public and the reliability required for software has become very high, while software has become increasingly complex and large-scale, and manual reviews, and Quality assurance through testing has become very difficult.

  Model checking technology describes the behavior of software in the input language of a specific model checker, and executes the specific model checker to comprehensively check the possible states of the software, thereby providing the properties that the software should have. This is a technique for determining whether or not the condition is satisfied (see, for example, Non-Patent Document 1). According to the method disclosed in Non-Patent Document 1, the behavior of software is described in an input language called Promela, and input to a model checker called SPIN, thereby performing inspection.

  Model checking technology is a promising technology for ensuring the quality of software that is becoming increasingly complex and large-scale. However, in order to comprehensively check the possible states of software, the number of states to be inspected for large-scale software There is a phenomenon called state explosion that becomes a huge amount. Due to this state explosion, the phenomenon that the time calculation amount necessary for processing becomes practically unacceptable, and the phenomenon that the space calculation amount necessary for processing exceeds the storage area installed in the computer used for processing, At least one of them may be caused and the above-described inspection may not be completed.

  In order to cope with the state explosion, a process called abstraction may be performed on the source code or the inspection code to reduce the number of states to a range that can be inspected. Abstraction includes, for example, simplification of branch conditions for selective execution statements. Since the abstraction may cause a situation where an originally nonexistent execution path occurs or an existing execution path disappears, there is a difference between the nature of the software indicated by the inspection result for the inspection code and the nature of the original software. Can be born. Therefore, it is desirable to apply abstraction after considering the level of abstraction in view of the property to be inspected for software.

  Further, in the model checking technique, it may be a practical problem that the labor for describing the software to be checked in the input language of the specific model checker is large. FIG. 35 shows an example of a source code conversion apparatus disclosed in Patent Document 1. According to the method disclosed in Patent Document 1, the source code is converted into the inspection code written in the input language of the specific model checker using the translation map (steps 910 to 940). According to the method disclosed in Patent Document 1, an inspection code is inspected by the specific model checker separately from the conversion using an environment model defined by a user (steps 975 and 950 to 970).

  One of the software development technologies is model-driven development. Model-driven development is a technology for advancing software development by describing software design information as a model and refining the model by a conversion operation. For example, in model-driven development, the format of the model and the meaning of the model are defined by a meta model described by the MOF (see, for example, Non-Patent Document 2), and conversion rules that detail the model are described by the QVT (for example, , Refer to non-patent document 3), description and verification of constraints on integrity and soundness of model are performed by OCL (for example, refer to non-patent document 4), and source code is generated from the model by MOFM2T (for example, non-patent document) Reference 5).

  Note that the “model” in model checking technology and the “model” in model-driven development are concepts that are independent of each other, and generally have no commonality in terms of data structure and meaning.

JP 2000-181750 A

G. J. Holzmann, "The Model Checker Spin," IEEE Transactions on Software Engineering, vol. 23, no. 5, pp. 279--295, May 1997 http://doi.ieeecomputersociety.org/10.1109/32.588521 The Object Management Group, "Meta Object Facility (MOF) Core Specification", formal / 06-01-01, January 2006, http://www.omg.org/spec/MOF/2.0/PDF The Object Management Group, "Meta Object Facility (MOF) 2.0 Query / View / Transformation Specification", formal / 2008-04-03, April 2008, http://www.omg.org/spec/QVT/1.0/PDF The Object Management Group, "Object Constraint Language", formal / 2006-05-01, May 2006, http://www.omg.org/spec/OCL/2.0/PDF The Object Management Group, "MOF Model to Text Transformation Language, v1.0", formal / 2008-01-16, January 2008, http://www.omg.org/spec/MOFM2T/1.0/PDF

  In order to effectively ensure software reliability through model checking, reduce the effort to obtain the checking code by automatically generating the checking code described in the input language of the model checker from the source code. In addition, it is necessary to abstract the specification and design of the software so that the exhaustive inspection by the model checker is completed with realistic time complexity and space complexity.

  According to the method disclosed in Patent Document 1, there is a problem that the reusability of the abstract description is low. According to the method disclosed in Patent Document 1, a translation map and an environment model, which are abstraction means necessary for model checking, are used when a new type of instruction such as a revision of a source program is introduced into the source code. Although limited, in the actual inspection, (1) not limited to the introduction of a new type of instruction, software design change (2) change of the abstraction method of the target software (3) inspection to different model checker There can be three types of changes corresponding.

  As examples of (1), there may be a change in association with an environmental model due to a change in software structure, and a change in procedure across a plurality of instructions. Software often involves structural changes with each revision, and this type of change is frequently added.

  As an example of (2), there are replacement of a random number or the like with a constant or non-deterministic value of a function, and simplification of processing. In realistic software model checking, a state explosion easily occurs, so abstraction according to the checking items and adjustment of the checking level itself are required.

  As an example of (3), there can be a change to a model checker capable of different inspections, and more simply a change to a model checker version change. Since each model checker has features, it is desirable to have multiple model checkers for effective inspection.

  According to the method disclosed in Patent Document 1, in any of the above-described three types of changes, a translation map that is a map from the language of the source code to the language of the model checker and the language of the model checker are described. At least one of the specified environmental models must be modified. Therefore, when a change is made for a certain purpose 1 (for example, a change in abstraction method) and a change is made for a different purpose 2 (for example, a design change), the translation map before these changes and If an attempt is made to change the purpose 2 and new purpose 3 (for example, change of the model checker) to the environmental model, the first change for purpose 2 cannot be reused. Changes that satisfy 3 must be made at the same time.

  The present invention provides a source code conversion method and a source code conversion program capable of flexibly changing an abstract description and reusing the abstract description efficiently based on the problems of the prior art. The purpose is to do.

  To show a typical example of the present invention, a source code executed by a source code conversion device that converts a software source code into an inspection code described in an input language of a verification tool using a plurality of different conversion rules. In the conversion method, the plurality of different conversion rules are obtained by dividing a series of processes for converting and abstracting the source code into the inspection code, and dividing the source code into the finer granularity. A first conversion rule for converting to an intermediate format which is a format independent of a specific programming language; a second conversion rule for abstracting the converted intermediate format; and converting the converted intermediate format into the inspection code A third conversion rule, wherein the method receives the source code and at least one input of the first conversion rule. Attaching the source code using the input first conversion rule; receiving the input of at least one second conversion rule; receiving the input of at least one third conversion rule; Converting to the intermediate format; abstracting the converted intermediate format using the input second conversion rule; and converting the intermediate format using the input third conversion rule. Converting the intermediate format into the inspection code, the intermediate format abstracting the converted intermediate format in addition to a physical element that is equivalent to an element of the source code or the inspection code It is possible to express a logical element that is an element generated in the step of performing.

  The effects obtained by the representative ones of the inventions disclosed in the present application will be briefly described as follows. That is, it is possible to provide a source code conversion method and a source code conversion program that can flexibly change the abstract description and that can efficiently reuse the abstract description.

It is a figure for demonstrating the basic concept of this invention. It is a figure explaining the input interface of the conversion rule in the source code conversion process of this invention. It is a figure which shows the structural example of the source code conversion system which becomes 1st Example of this invention. It is a figure which shows the structural example of the source code converter in the conversion system of FIG. 3A. It is a figure which shows the example of the processing flow of 1st Example of this invention. It is a figure which shows an example of input operation with respect to a source code converter. It is a figure which shows the other example of input operation with respect to a source code converter. It is a figure explaining operation | movement of a source code converter. It is a figure explaining the procedure of source code conversion in detail. It is a figure which shows an example of the abstraction of a model. It is a figure which shows an example of the abstraction of a model. It is a figure which shows an example of the meta and mounting model in 1st Example of this invention. It is a figure which shows an example of the meta generalization model in 1st Example of this invention. It is a figure which shows an example of the meta and verification model in 1st Example of this invention. It is a figure which shows the source code in the 1st conversion example in the 1st Example of this invention. It is a figure which shows the test | inspection code in the 1st conversion example in 1st Example of this invention. It is a figure which shows the mounting model in the 1st conversion example in 1st Example of this invention. It is a figure which shows the first generalization model in the 1st conversion example in the 1st Example of this invention. It is a figure which shows the 2nd generalization model in the 1st conversion example in 1st Example of this invention. It is a figure which shows the test | inspection model in the 1st conversion example in 1st Example of this invention. It is a figure which shows the source code in the 2nd conversion example in the 1st Example of this invention. It is a figure which shows the source code in the 3rd conversion example in the 1st Example of this invention. It is a figure which shows the mounting model in the 2nd conversion example in 1st Example of this invention. It is a figure which shows the mounting model in the 3rd conversion example in 1st Example of this invention. It is a figure which shows the first generalization model in the 2nd conversion example in 1st Example of this invention. It is a figure which shows the first generalization model in the 3rd conversion example in 1st Example of this invention. It is a figure which shows the test | inspection code in the 4th conversion example in 1st Example of this invention. It is a figure which shows the test | inspection model in the 4th conversion example in 1st Example of this invention. It is a figure which shows the source code in the 5th conversion example in the 1st Example of this invention. It is a figure which shows the test | inspection code in the 5th conversion example in 1st Example of this invention. It is a figure which shows the mounting model in the 5th conversion example in 1st Example of this invention. It is a figure which shows the first generalization model in the 5th conversion example in 1st Example of this invention. It is a figure which shows the 2nd generalization model in the 5th conversion example in 1st Example of this invention. It is a figure which shows the 3rd generalization model in the 5th conversion example in 1st Example of this invention. It is a figure which shows the test | inspection model in the 5th conversion example in 1st Example of this invention. It is a figure which shows the example of the processing flow of the source code converter which becomes the 2nd Example of this invention. It is a figure explaining the procedure of verification of the validity of conversion in the 3rd Example of this invention in detail. It is a figure which shows an example of the source code conversion apparatus of a prior art example.

  In the present invention, the source code to be inspected is converted into the inspection code described in the input language of the model checker using a plurality of different conversion rules. The plurality of different conversion rules are obtained by converting a source code to be inspected into an inspection code described in an input language of a model checker, and dividing a series of abstraction processes into fine granularities. By using in combination, conversion from the source code to the inspection code is realized.

  In the present invention, a series of processing for converting a source code to be inspected into an inspection code is divided into fine granularities including abstraction processing, and each divided is referred to as a “conversion rule”. The source code conversion apparatus realized by the present invention has an interface for selecting or inputting a plurality of different conversion rules by a user when converting a source code into an inspection code. The conversion rule is input by one of a selection from a plurality of conversion rules stored in advance in the source code conversion apparatus and a user description.

  In the present invention, the conversion rule includes an implementation-generalization conversion rule for converting source code into a format having generalized program information (generalization model) independent of the description language of the source code, The generalized model is classified into an abstraction conversion rule for abstracting a generalized model and a generalization-check conversion rule for converting a generalized model into a description language of a model checker. In other words, the plurality of different conversion rules include a first conversion rule for converting source code into an intermediate format that is a format independent of a specific programming language, and a second conversion rule for performing an abstraction process on the intermediate format. And a third conversion rule for converting the intermediate format into the inspection code. The conversion from the source code to the inspection code includes the steps of converting the source code into a generalized model by an implementation-generalization conversion rule, abstracting the generalization model by an abstraction conversion rule, and the generalization model. This is realized by successively performing the three steps of converting the generalized model into a test code according to the generalization-check conversion rule. In other words, for the conversion from the source code to the inspection code, the step of inputting one or more of each of the first, second, and third conversion rules, and the software source code using the first conversion rule, Converting to the intermediate format; using the second conversion rule to abstract the software expressed in the intermediate format; and using the third conversion rule to input the intermediate format to the verification tool This is realized by continuously performing the three steps of converting into the verification code described in the language.

  In the present invention, the information (model) held internally in a series of processes for converting the source code to be inspected into the inspection code is defined by the meta model. The model is classified into an implementation model having information corresponding to the source code to be inspected, the generalization model described above, and an inspection model having information corresponding to the description language of the model checker. The implementation model is defined by the meta / implementation model that is the metamodel, the generalization model is defined by the meta / generalization model that is the metamodel, and the inspection model is defined by the meta / inspection model that is the metamodel. Defined. Each of the above-described metamodels has a definition of a data structure and information on constraints between elements included in the data.

  In the present invention, the generalization model includes two types of elements: a physical element having an equivalent element corresponding to an element of the mounting model or the inspection model, and a logical element used in the process of abstraction conversion. included. A logical element is an element inheriting the characteristics of a physical element that can have attribute information and a reference to a related physical element. Each physical element has a corresponding logical element. For example, by describing as a conversion rule, giving additional attribute information by replacing a physical element with a corresponding logical element, replacing with a new logical element, and replacing a logical element with a different physical element The abstract description can be reused at each stage.

  Hereinafter, embodiments of the present invention will be described in detail with reference to the drawings.

  First, the basic concept of the present invention will be described with reference to FIGS. In the present invention, as shown in FIG. 1, the source code 0001 is subjected to a conversion process in which a plurality of conversion rules 0002 are combined in the source code conversion apparatus 1000, so that the inspection code 0005 suitable for the existing model inspection apparatus Convert to That is, (a) “conversion” is divided into fine granularities and packaged as a combination of a plurality of “conversion rules” 0002, thereby realizing flexible conversion. (B) The user (inspector) inputs the source code 0001 to be inspected, selects the “conversion rule” 0002 corresponding to the target source code and the inspection level, and obtains the desired inspection code 0005.

Examples of the “conversion rule” in the present invention are as follows.
(A) Convert simple syntax conversion "C language conditional branch (If statement / Switch statement)" into "check code conditional branch (If statement)""C language repetition statement (for statement, while statement, ... ) ”Is converted to“ Repeated inspection code (Do statement) ”(b) Modeling of external environment“ Read data ”is replaced with“ Random input ”(c) Abstraction“ Repeat removal ”
"Simplification of conditions"
The conversion rule input interface in the source code conversion processing of the present invention will be described with reference to FIG.

  According to the present invention, since the interface for inputting a plurality of conversion rules 0002 divided into fine granularities is owned, the abstraction can be easily changed by the user by selecting and inputting a plurality of different conversion rules 0002. Realized. In other words, the user can change the abstraction level by selecting a plurality of different conversion rules 0002 according to the domain information, the property to be inspected, and the information on the inspection level (influence on the property due to abstraction). And can be easily realized by an operation to be input to the source code conversion apparatus 1000.

  The present invention includes a procedure for converting the source code 0001 to be inspected into the inspection code 0005 described in the input language of the model checker using a plurality of different conversion rules 0002. The plurality of different conversion rules are classified into an implementation-generalization conversion rule, an abstraction conversion rule, and a generalization-inspection conversion rule, and conversion using these conversion rules is executed in stages. When following the design change of the source code to be inspected, only the conversion rule related to the change needs to be changed, and the change is minimized. In addition, the implementation model, the generalization model, and the inspection model are each defined in the meta model, and by adding constraints, it is possible to verify that the conversion result by the conversion rule is not illegal. Thus, in this embodiment, a series of processes for converting the source code to be inspected while abstracting it into the inspection code is realized by combining fine-grained conversion rules. A method for realizing such a series of processes It is possible to prevent an increase in the verification cost of the conversion rule caused by.

  In addition, in order to inspect with a different inspection tool, when outputting in the format of the inspection tool, only the meta / inspection model and the generalization-inspection conversion rule need be created, and the creation part is minimized. It is done.

(First embodiment)
Next, a source code conversion apparatus and conversion processing method according to the first embodiment of the present invention will be described with reference to FIGS. 3A to 32.

  FIG. 3A is a diagram illustrating a configuration example of a source code conversion system including a source code conversion apparatus according to the first embodiment. A source code conversion apparatus 1000 applied to an embodiment of the present invention is an apparatus that converts a source code 0001 to be inspected into an inspection code 0005, and includes an input unit 1100, a conversion processing unit 1200, an output unit 1300, and a storage. Unit 1400 and control unit 1500. Reference numeral 2000 denotes a model inspection tool, and reference numeral 3000 denotes an inspection result.

  The input unit 1100 receives input of the source code 0001 and the conversion rule 0002. The storage unit 1400 stores a conversion rule 0002, a meta model 0003, and a writing rule 0004. The meta model 0003 is data for defining a model format internally held in a series of processes for converting the source code 001 into the inspection code 0005 by the conversion processing unit 1200. As described above, the meta model 0003 holds the definition of the data structure and information on the constraints between the elements included in the data. The elements included in the data include physical elements and logical elements. Information regarding the physical elements is referred to as a physical element definition 0031, and information regarding the logical elements is referred to as a logical element definition 0032.

  The conversion processing unit 1200 converts the source code 0001 to be inspected into the inspection code 0005 based on the conversion rule 0002. The output unit 1300 outputs the inspection code 0005 based on the writing rule 0004. The control unit 1500 is a processor that executes various processes for controlling the entire process of the source code conversion apparatus 1000.

  FIG. 3B shows a configuration example of the source code conversion apparatus 1000. The input unit 1100 includes a source code input unit 1101 and a conversion rule input unit 1102. The conversion processing unit 1200 includes a model construction unit 1201, an implementation-generalized model conversion unit 1202, an abstract model conversion unit 1203, and a generalization-check model conversion unit 1204. The output unit 1300 includes an inspection code writing unit 1301. The storage unit 1400 includes a conversion rule database 1401, a metamodel database 1402, and a writing rule database 1403.

  The source code conversion apparatus 1000 is implemented, for example, as a program that operates on a single computer or a plurality of computers connected via a network. The source code 0001 and the conversion rule set 0002 are input by a method such as a method of reading from a storage device on a computer and a method of directly inputting by an input device connected to the computer. The inspection code 0005 is output by, for example, a method of writing to a storage device on a computer and a method of displaying on a display device of a computer.

  The input unit 1100 receives data input by the user and performs a process of supplying the input data to the conversion processing unit 1200. The input unit 1100 receives information related to the source code 0001 and a plurality of conversion rules divided into fine granularities, that is, information related to the “conversion rule set” 0002, and supplies the information to the conversion processing unit 1200. In an embodiment, the input unit 1100 may receive an instruction from the user regarding driving and control of the conversion processing unit and driving and control of the output unit.

  Information about the source code 0001 and information about the conversion rule set 0002 to be applied to the source code 0001 are supplied to the conversion processing unit 1200 from the input unit 1100. In addition, the conversion processing unit 1200 performs processing for converting the source code 0001 by the conversion rule set 0002, and supplies information on the conversion result to the output unit 1300. In an embodiment, the information related to the conversion rule set 0002 supplied from the input unit 1100 includes only identification information indicating the conversion rule 0002 stored in the storage unit 1400. The identification information may be taken out from the storage unit 1400 and used for conversion.

  Details of the conversion processing unit 1200 and the output unit 1300 will be described with reference to FIG.

  The conversion processing unit 1200 includes a model construction unit 1201, an implementation-generalized model conversion unit 1202, an abstract model conversion unit 1203, and a generalization-check model conversion unit 1204.

  In the present embodiment, the conversion processing unit 1200 converts the source code information 1001 into the inspection model 1008 by model conversion using the meta model 0003 (see FIG. 3A) and the conversion rule 0002. The meta / implementation model 1002, the meta / generalization model 1003, and the meta / inspection model 1004 are described in, for example, the MOF described in Non-Patent Document 2. Also, for example, in the QVT described in Non-Patent Document 3, the implementation-generalization conversion rule 1005, the abstraction conversion rule 1006, and the generalization-inspection conversion rule 1007 are described, and the model is converted. . The conversion may be another model conversion method already exemplified, or a plurality of methods may be mixed.

  In some embodiments, the implementation-generalization model conversion unit 1202, the abstraction model conversion unit 1203, and the generalization-check model conversion unit 1204 may be performed by the same part without being independent of each other. Further, the meta / implementation model 1002, the meta / generalization model 1003, and the meta / inspection model 1004 are individually meta-models of the implementation model 1205, the generalization model 1206, and the inspection model 1008. The mounting model 1205, the generalization model 1206, and the inspection model 1008 may be defined by a single meta model without preparing. In one embodiment, the meta / implementation model 1002, the meta / generalization model 1003, and the meta / inspection model 1004 are implemented by a plurality of methods, respectively, an implementation model 1205, a generalization model 1206, and an inspection model 1008. You may define the form and constraints. For example, each meta model includes the constraint conditions described in the OCL described in Non-Patent Document 4 in addition to the definition by the MOF, and satisfies the constraint conditions when the model is converted. There can be a method of verifying whether or not.

  The model construction unit 1201 receives the source code information 1001 from the source code input unit 1101 and converts it into the implementation model 1205. The format of the mounting model 1205 is defined by a meta / implementation model 1002 that is the meta model. The implementation model 1205 preferably has sufficient information necessary for mutual conversion with the source code information 1001 in order to obtain the effects of the present invention to the maximum. However, in some embodiments, an inspection code is output. Information may be omitted or added as long as the purpose of doing so is not lost.

  In an embodiment, the model construction unit 1201 may be implemented in a manner inseparable from the source code input unit 1101 and the process may proceed in a form in which the source code information 1001 does not occur.

  The mounting-generalization model conversion unit 1202 converts the mounting model 1205 into the generalization model 1206 using the mounting-generalization conversion rule 1005, the meta / mounting model 1002, and the meta / generalization model 1003. The generalization model 1206 has a data structure that can represent structures and processes in a plurality of programming languages. For example, in the generalization model 1206, the If statement and the Switch statement in the source code 0001 are not distinguished from each other and are expressed as selective execution statements. In an embodiment, when the mounting model 1205 is converted into the generalization model 1206, only the mounting-generalization conversion rule 1005 may be used. In some embodiments, when the implementation-generalization conversion rule 1005 includes a plurality of conversion rules, the plurality of conversion rules are integrated into one conversion rule, and the implementation model 1205 to the generalization model 1206 There can be a method used for conversion. In one embodiment, when the implementation-generalization conversion rule 1005 includes a plurality of conversion rules, a procedure for converting the implementation model 1205 to the generalization model 1206 by repeating the conversion process a plurality of times is provided. possible.

  The abstraction model conversion unit 1203 abstracts the generalization model 1206 using the abstraction conversion rule 1006 and the meta / generalization model 1003. As an example of abstraction, there may be a method of replacing a conditional expression in a selection statement with a true, false, or non-deterministic selection. In an embodiment, when abstracting the generalization model 1206, only the abstraction conversion rule 1006 may be used. Further, in an embodiment, when the abstraction conversion rule 1006 includes a plurality of conversion rules, there is a method of integrating the plurality of conversion rules into one conversion rule and using it for the abstraction of the generalization model 1206. obtain. In an embodiment, when the abstract conversion rule 1006 includes a plurality of conversion rules, there may be a procedure for converting the generalized model 1206 by repeating the conversion process a plurality of times.

  The generalization-inspection model conversion unit 1204 converts the generalization model 1206 into an inspection model 1008 using the generalization-inspection conversion rule 1007, the meta / generalization model 1003, and the meta / inspection model 1004. For example, when the inspection code 0005 is in the Promela format, an element expressed as a selective executable statement in the generalization model is expressed as an If statement in the inspection model. In an embodiment, when the generalization model 1206 is converted into the inspection model 1008, only the generalization-inspection conversion rule 1007 may be used. Further, in a certain embodiment, when the generalization-inspection conversion rule 1007 includes a plurality of conversion rules, the plurality of conversion rules are integrated into one conversion rule, and the generalization model 1206 to the inspection model 1008 are integrated. There can be a method used for conversion. Further, in a certain embodiment, when the generalization-inspection conversion rule 1007 includes a plurality of conversion rules, a procedure for converting the generalization model 1206 to the inspection model 1008 by repeating the conversion processing a plurality of times is provided. possible.

  The output unit 1300 outputs the inspection code 0005 using the conversion result information supplied from the conversion processing unit 1200. In an embodiment, when the inspection code 0005 is output, information such as grammar information of the description language of the model checker may be supplied from the storage unit 1400, for example.

  The inspection code writing unit 1301 converts the inspection model 1008 into the inspection code 0005 using the meta / inspection model 1004 and the inspection code writing rule 1009 acquired from the writing rule database 1403 of the storage unit 1400. For example, the inspection code writing rule 1009 is described by the method described in Non-Patent Document 5, and the inspection model 1008 is converted to the inspection code 0005. In an embodiment, the present invention is not limited to this, and any method for converting the inspection model 1008 into a description format of a model checker used for inspection may be used. For example, when SPIN is used as a model checker, the inspection code 0005 is described in the Promela language, which is the SPIN input language.

  In the storage unit 1400, each of the conversion rule database 1401, the metamodel database 1402, and the writing rule database 1403 is an arbitrary data storage method realized on a computer, such as a relational database or a hierarchical database. Realized. The conversion rule database 1401, the metamodel database 1402, and the writing rule database 1403 do not have to be implemented by the same method, and may be implemented by different methods. In addition, each of the conversion rule database 1401, the metamodel database 1402, and the writing rule database 1403 does not have to be realized by a single method. For example, a part of information to be held is a relational database. A part of the information to be stored and held may be realized by a combination of different methods, for example, incorporated in a computer program for realizing the invention.

  The storage unit 1400 supplies information necessary for the input unit 1100, the conversion processing unit 1200, and the output unit 1300 to perform respective processes. For example, the storage unit 1400 stores information on conversion rules, information on metamodels, and information on grammar of a model checker description language.

  As described above, the conversion rule database 1401 holds conversion rules together with metadata. The metadata is for selecting a conversion rule, and there may be a method having different information of the implementation-generalization conversion rule 1005, the abstraction conversion rule 1006, and the generalization-inspection conversion rule 1007. . The metadata of the implementation-generalization conversion rule 1005 can be, for example, the type of description language of the conversion source code. The metadata of the abstraction conversion rule 1006 includes, for example, a name that simply represents the abstraction in a straightforward manner, a brief description, an abstraction type such as “data abstraction”, “processing abstraction”, and a natural language ( For example, there are state number reduction effect by abstraction expressed in alphabet or numerical value, influence on properties by abstraction expressed in natural language (for example, alphabet or numerical value), and software domain to which abstraction can be applied The metadata of the generalization-inspection conversion rule 1007 may have a name indicating a model checker used for inspection, for example.

  Hereinafter, the details of the input unit 1100, the conversion processing unit 1200, the output unit 1300, the storage unit 1400, and the control unit 1500 will be described with reference to FIGS.

  First, an example of the source code conversion procedure in the present embodiment will be described with reference to FIGS. The source code conversion procedure in this embodiment includes a source code input step S101, a conversion rule input step S102, a conversion rule application step S103, and an inspection code output step S104. This source code conversion procedure is executed mainly by the control unit 1500.

  First, in the source code input step S101, the source code 0001 is read into the source code conversion apparatus 1000 by the source code input unit 1101 and converted into the source code information 1001.

  The source code input unit 1101 receives the source code 0001 to be inspected input from the user, and converts it into source code information 1001. The source code 0001 is described in, for example, a programming language C published in JIS X3010-1993. Specifically, the source code information 1001 is held, for example, in the form of an abstract syntax tree. The format of the source code information 1001 is not limited to an abstract syntax tree, and may be any format that holds information required for the inspection of the source code 0001 such as structure and logic.

  Subsequent to the source code input step S101, in the conversion rule input step S102, the conversion rule input unit 1102 reads the conversion rule set 0002, which is a plurality of conversion rules divided into fine granularities, into the source code conversion apparatus 1000. In this conversion rule input step S102, at least one of a correspondence relationship between the model element before conversion and the model element after conversion, and an operation applied to the element of the model before conversion by conversion is defined. The process of reading the conversion rule set 0002 into the source code conversion apparatus 1000 is not necessarily performed by a single operation by the user, and may be performed by a repetitive operation. Further, the source code input step S101 and the conversion rule input step S102 are not necessarily completed in this order, and the source code 0001 is input before the source code information 1001 is generated by the source code input unit 1101. In addition, the source code 0001 may be input before the conversion rule input unit 1102 requests the source code information 1001 for the conversion rule input process. Therefore, the processing may proceed in the order in which the processing of the source code input step S101 and the processing of the conversion rule input step S102 are mixed. For example, the source code input unit 1101 receives the source code 0001, then the conversion rule input unit 1102 receives the conversion rule set 0002, and then the source code input unit 1101 transfers the source code 0001 to the source code information 1001. There can be a procedure to convert.

  The conversion rule input unit 1102 accepts a conversion rule set 0002 input from a user. As a method for receiving the conversion rule set 0002 from the user, for example, there may be the following method.

  As an example of the first conversion rule input method, the conversion rule input unit 1102 receives a conversion rule that is directly input by a user manually as part of the conversion rule set 0002.

  As an example of the second conversion rule input method, as shown in FIG. 5A, at least a part of the conversion rule set 0002 may be input by a conversion rule (description) 0010 described by the user. Also, the input unit 1100 acquires the conversion rule list 0015 from the storage unit 1400, presents the acquired conversion rule list 0015 to the user in the form of a list or the like, and the conversion rule is displayed from the presented list to the user. May select the conversion rule set 0002. That is, the user inputs (describes) the conversion rule search condition 0011 to the conversion rule input unit 1102 of the input unit 1100 before the input of the conversion rule, and then the conversion rule input unit 1102 Conversion rules that match the search conditions are acquired from the conversion rule database 1401 of the storage unit 1400 and presented to the user as a conversion rule list 0015. Subsequently, the user selects one or more conversion rules included in the presented conversion rule list 0015. The conversion rule input unit 1102 accepts one or more conversion rules selected by the user as a part of the conversion rule set 0002.

  As an example of the third conversion rule input method, first, the user inputs the conversion rule search condition 0011 to the conversion rule input unit 1102 before the conversion rule input, and then the conversion rule input unit. 1102 may acquire a conversion rule that matches the search condition from the conversion rule database 1401 and accept it as a part of the conversion rule set 0002.

  As an example of the fourth conversion rule input method, as shown in FIG. 5B, the conversion rule input unit 1102 extracts and generates the conversion rule search condition 0012 from the input source code 0001, and further, the search condition Is obtained from the conversion rule database 1401 and accepted as a part of the conversion rule set 0002.

  Examples of the conversion rule search condition factor in the second conversion rule input method example, the third conversion rule input method example, and the fourth conversion rule input method example are the conversion rule database described later. At 1401, there may be information stored as metadata for the conversion rule.

  As an example of the fifth conversion rule input method, the conversion rule input unit 1102 accepts a conversion rule by processing the conversion rule input by some method. As an example of the processing method, the conversion rule database 1401 holds the conversion rule in a state in which the variable name or the like in the source code 0001 is parameterized, for example, by a method by explicit input of the user, There may be a method of including the parameter embedded with the information of the source code 0001 in the conversion rule set 0002. In the fifth conversion rule input method example, the conversion rule input method for the processing source is the same as the case of using the input conversion rule without processing, such as the first conversion rule input method described above. There can be a method.

  The method by which the conversion rule input unit 1102 receives the conversion rule set 0002 is not limited to these conversion rule input methods, and any method that receives a set of conversion rules used by the conversion processing unit 1200 may be used. The conversion rule set 0002 may be received by one or more combinations of input methods.

  Following the conversion rule input step S102, in the conversion rule application step S103, the model construction unit 1201 converts the source code information 1001 into the mounting model 1205, and then the mounting-generalization model conversion unit 1202 generalizes the mounting model 1205. Next, the abstract model conversion unit 1203 abstracts the generalized model 1206 (S1032), and then the generalization-check model conversion unit 1204 converts the generalized model 1206 to the check model 1008. (S1033). The conversion rule input step S102 and the conversion rule application step S103 do not necessarily have to be completed in this order, and the implementation-generalization conversion rule 1005 is input before the processing of the implementation-generalization model conversion unit 1202. The abstraction conversion rule 1006 may be input before the process of the abstraction model conversion unit 1203, and the generalization-check conversion rule 1007 may be input before the process of the generalization-check model conversion unit.

  Subsequent to the conversion rule applying step S103, in the inspection code output step S104, the inspection code writing unit 1301 writes the inspection model 1008 as the inspection code 0005. The designation of the writing destination of the inspection code 0005 does not necessarily have to be after the conversion rule applying step S103, and may be any earlier than the writing of the inspection code 0005. For example, there may be a procedure in which the designation of the writing destination of the inspection code 0005 is performed in parallel with the source code input step S101.

  Next, the conversion procedure will be described in more detail with reference to FIGS. 7, 8A, and 8B. As shown in FIG. 7, in the present invention, the following processing is performed in order to perform conversion step by step using a model conversion technique.

(1) Source code 0001 is converted into (almost) equivalent “implementation model” 1205 (2) “implementation model” is expressed in program format such as structure and logic in a format independent of a specific programming language Conversion to “generalization model” 1206 In other words, using at least one of a plurality of different first conversion rules 1005-1 to 1005-n, the “implementation model” 1205 is an intermediate format that is a format independent of a specific programming language. Conversion into “generalization model” 1206. In the example of FIG. 7, as the first conversion rule, ““ if statement ”→ conditional branch”, ““ switch statement ”→ conditional branch”, ““ while statement ”→“ repeat ””, and ““ for statement ”→ At least four different conversion rules “Repeat” are selected.

(3) Conversion for abstraction is performed on the generalization model 1206. That is, using at least one of a plurality of different second conversion rules 1006-1 to 1006-n, the generalized model in the intermediate format Abstraction processing is performed on 1206. In the example of FIG. 7, at least two different conversion rules of “data reading → random input” and “data abstraction” are selected as the second conversion rule.

(4) The generalization model 1206 is converted into an “inspection model” 1008 to generate a code (output)
That is, by using at least one of a plurality of different third conversion rules 1007-1 to 1007-n, the generalized model 1206 in the intermediate format is converted into the inspection model 1008 having information necessary for generating the inspection code. In the example of FIG. 7, as the third conversion rule, there are at least two different conversion rules corresponding to the first conversion rule: ““ conditional branch ”→“ if ”sentence” and ““ repeat ”→“ do ”sentence”. Is selected.

  The implementation model 1205, the generalization model 1206, and the inspection model 1008 each have a data structure and semantics defined by a “meta model” that defines the syntax.

  As described above, when converting from the mounting model 1205 to the generalized model 1206, for example, when the grammar of the description language of the source code to be converted includes “for sentence” and “while sentence” as the notation of the iterative process, A person selects a rule for converting “for sentence” to “repetition” and a rule for converting “while sentence” to “repetition” as the first conversion rule using the conversion rule input method described above. When converting the abstraction of the generalization model 1206, the user determines the inspection level (degree of abstraction), and as a conversion rule for achieving the determined inspection level, for example, an instruction and a series of processing related to reading of external data Are selected as the second conversion rule 1006 by using the conversion rule input method described above, and the rule for converting a specific data type to a higher abstract type. Furthermore, when converting from the generalized model 1206 to the check model 1008, for example, when the grammar of the input language of the model checker has “do sentence” as a notation of repetition processing, the user sets “repetition” to “do sentence”. The rule to be converted to “” is selected as the third conversion rule 1007 using the conversion rule input method described above. As the conversion rules, those that can be used repeatedly, such as general-purpose rules that can be applied across a plurality of software, are stored in a database. The conversion rules stored in the database have domain information and information on inspection level (influence on inspection by abstraction) as meta information used as a judgment material for search and rule selection by the user.

  The conversion rule selection method includes the following.

(1) General-purpose rules: always selected (2) Rules dependent on a specific library: Selection by entering the library used and the domain (category) to be inspected (3) Rules corresponding to abstraction : Automatically generated from the list of conversion rules (obtained by inputting the property / inspection level to be inspected) selected by the user, entered by the user himself / herself, or the property to be inspected

  8A and 8B show examples of model abstraction. The model abstraction can reduce the number of states. However, abstraction can affect the properties of the model. For example, the detected defect (counterexample) does not exist in the original system, or a defect present in the original system cannot be found. On the other hand, a sound abstraction that does not affect properties tends to have a small effect on the number of states.

  9 shows a part of an example of the meta / implementation model 1002, FIG. 10 shows a part of an example of the meta / generalization model 1003, and FIG. 11 shows a part of an example of the meta / inspection model 1004. The meta / implementation model 1002, the meta / generalization model 1003, and the meta / inspection model 1004 in the present embodiment are shown using the notation disclosed in Non-Patent Document 2. For example, in FIG. 9, the IfStatement class C101 is shown to inherit the Statement class C102 by the relationship R101, and the relationship R102 shows that the Expression class C103 is owned as the attribute condition, and the relationship R103 shows that the attribute body It is shown that the set of Statement class C102 is owned, and the relationship R104 shows that the set of Statement class C102 is owned as attribute elseBody. Further, for example, in FIG. 9, the IntegerConstant class C104 is shown to possess an attribute value that is an integer value, and the relationship R105 indicates that the Expression class C103 is inherited. Further, for example, in FIG. 9, the VariableReference class C105 is shown to inherit the Expression class C103 by the relationship R106, and the relationship R107 indicates that the VariableDeclaration class C106 is referred to.

  Each element of the meta / implementation model 1002 and each element of the meta / inspection model 1004 include language elements of the implementation programming language and elements corresponding to the language elements of the inspection language. In this embodiment, the implementation programming language is C language, and the inspection language is Promela language. Therefore, the meta / implementation model 1002 includes elements that correspond to C language elements, and the meta / inspection model. Reference numeral 1004 includes an element associated with the language element of the Promela language. For example, the IfStatement class C101 in FIG. 9 represents an If statement in C language, and the IntegerConstant class C104 represents an integer type constant value in C language.

  The meta / generalization model 1003 shown in FIG. 10 is an element that is semantically associated with an element included in the meta / implementation model 1002 or an element that is semantically associated with an element included in the meta / inspection model 1004. A physical element is included. In the meta / generalization model 1003 in this embodiment, the physical element is expressed as an element that inherits the PhysicalElement class C201 transitively in FIG. For example, the Statement class C203 and the SelectionStatement class C204 are examples of physical elements. Each physical element does not have to have a one-to-one correspondence with an element included in the meta / implementation model 1002 or an element included in the meta / inspection model 1004. It only needs to be able to express the element. For example, in this embodiment, a C language If statement expressed as an IfStatement class C101 in the meta / implementation model 1002 is expressed by a combination of the SelectionStatement class C204 and the SelectionItem class C205 in the meta / generalization model 1003.

  In addition to the physical elements described above, the meta / generalization model 1003 includes logical elements that allow the elements associated with the conversion rules to be changed according to the nature of the source code, the purpose of the conversion, and the constraint conditions. In this embodiment, the logical element is expressed as an element that transitively inherits the LogicalElement class C202 in FIG.

  The LogicalElement class C202 owns a set of Attilibute class C206. The Attribute class C206 has a function of adding attribute information to classes and methods. Thus, a certain conversion rule can add additional attribute information to the converted logical element by converting a certain physical element into a logical element. Also, the added attribute information can be used by different conversion rules.

  The LogicalElement class C202 owns a set of RelatedElement classes C207 that can refer to arbitrary physical elements. This allows a transformation rule to add a relationship to an arbitrary element to the logical element along with the name of that association, and other transformation rules can utilize the association.

  Also, a logical element is defined for each physical element, such as a Logical_Statement class C208 for the Statement class C203. For this reason, the conversion rule can convert an arbitrary physical element into a logical element obtained by adding information or a relation to the physical element. In addition, since all logical elements inherit some physical element, after a certain physical element is converted to a logical element in a certain conversion rule, it is conscious that it is a logical element in a different conversion rule. It can also be handled as a physical element.

  For example, the following conversion rules using logical elements may include the following methods (1) to (3).

  (1) A physical element of a generalization model that matches a certain pattern is converted into a logical element having a certain structure (or a combination of a logical element and a physical element).

  (2) A logical element (or a combination of a logical element and a physical element) that matches a certain pattern is converted into a logical element (or a combination of a logical element and a physical element) having a different structure.

  (3) A logical element matching a certain pattern (or a combination of a logical element and a physical element) is converted into a physical element.

  The generalization model 1206 may be converted into the inspection model 1008 after the logical elements are completely converted into physical elements on the generalization model 1206. The generalization model 1206 including a logical element may be directly converted into the inspection model 1008 using a conversion rule that can convert the logical element of the generalization model 1206 into the element of the inspection model 1008. In addition, the logical elements in the first to fifth conversion examples to be described later of the present embodiment express the random number generation method and the non-deterministic value selection method. Any element exceeding the range that can be directly expressed may be expressed. Examples of concepts expressed by logical elements include, for example, abstraction of exchanges with external environments such as hardware operations, abstraction of data structures and modules, and the like.

  Each meta model is not limited to those shown in FIGS. 9 to 11, and may be in any format that can represent a program to be converted. In addition, the logical elements in the generalization model 1206 are not limited to this, and the elements indicating the types of logical elements, logical elements, and other elements (physical elements or logical elements) necessary for describing the conversion rules Any notation that can express the element indicating the relationship may be used. In addition, the logical element may define a structure in advance for a specific frequent element. As an example of the definition of such a logical element, there may be a definition of a new class that has a maximum value and a minimum value as attributes, and that logically indicates random number generation and inherits the LogicalElement class C202 transitively. . Details of the logic element indicating the random number generation will be described with reference to FIG.

  Thereafter, the first conversion from the source code 0001 to the inspection code 0005 using the meta / implementation model 1002 shown in FIG. 9, the meta / generalization model 1003 shown in FIG. 10, and the meta / inspection model 1004 shown in FIG. Examples to a fifth conversion example are shown in FIGS.

  A first conversion example from the source code 0001 to the inspection code 0005 will be described with reference to FIGS.

  FIG. 12 is an explanatory diagram of an example of the C language source code 0001.

  In the line 001 of the source code 0001 shown in FIG. 12, a random value from 1 to 50 is generated by adding 1 to the remainder of dividing the return value of the function rand () that generates a random integer value by 50. Is done. In line 002, the function do_something () is executed with the random value generated in line 001 as an argument.

  FIG. 13 is an explanatory diagram of an example of the inspection code 0005 in the Promela language.

  In line 001 of the inspection code 0005 shown in FIG. 13, an integer type variable val is defined. In line 002, the value of the variable val is selected from integers from 1 to 50. In line 003, the function do_something () is executed with the value of the variable val selected in line 002 as an argument.

  FIG. 14 is an example of an implementation model 1205 of the source code 0001 shown in FIG.

  The mounting model 1205 shown in FIG. 14 is expressed using the definition by the meta / mounting model 1002 shown in FIG. For example, in the line 001 of the source code 0001 shown in FIG. 12, since the variable val is declared as an int type, the declaration has “val” as the attribute name in the implementation model 1205 shown in FIG. It is expressed as a VariableDeclaration element O0101 having “int” as the type.

  Also, the reference to the variable val in the line 002 of the source code 0001 shown in FIG. 12 is expressed by connecting the VariableDeclaration element O0101 and the VariableReference element O0102 via the link L0101 having the declaration as a label.

  14 implements the implementation-generalization conversion rule 1005 (first conversion rule 1005-1 shown in FIG. 7) that converts “for statement” and “while statement” into “repetition”. The result of conversion to the generalized model 1206 is shown in FIG. FIG. 15 is an explanatory diagram of the generalized model 1206 abstracted from the source code 0001 shown in FIG. Since the source code 0001 shown in FIG. 12 does not include “for statement” and “while statement”, the conversion is not executed, and the generalization model 1206 shown in FIG. 15 is substantially the same as the implementation model 1205 shown in FIG. Are the same.

  Next, the generalization model 1206 shown in FIG. 15 is converted by the abstraction conversion rule 1006 (second conversion rule 1006-1 shown in FIG. 7) shown in FIG. 6 which abstracts the random number generation processing and converts it into logical elements. The generalized model 1206 is shown in FIG. FIG. 16 shows the abstraction result of the generalization model 1206 shown in FIG.

  In the conversion process based on the abstraction conversion rule 1006, the BinaryOperation element O0401 shown in FIG. 15 and the element set owned by the BinaryOperation element O0401 transitively are an Attribute element O0702 indicating the minimum value 1 and an Attribute element O0703 indicating the maximum value 50. Is converted into a logical element (Logical_Expression element O0701) that means a random number generation expression that owns.

  The abstracted generalization model 1206 shown in FIG. 16 is converted into the inspection model 1008 by the generalization-inspection conversion rule 1007 (third conversion rule 1007-1 shown in FIG. 7) shown in FIG. Shown in FIG. 17 is an explanatory diagram of the inspection model 1008 converted from the abstracted generalized model 1206 shown in FIG.

  The combination of the Logical_Expression element O0701, which is the logical element shown in FIG. 16, the Attribute element O0702 representing the minimum value, and the Attribute element O0703 representing the maximum value represents a select statement that assigns a nondeterministic value in the Promela language. To a combination of a SelectStatement element O0801, an IntegerConstant element O0802 meaning a minimum value, and an IntegerConstant element OO803 meaning a maximum value. The IntegerConstant element O0802 is connected to the SelectStatement element O0801 via a link L0801 having min as a label. The IntegerConstant element O0803 is connected to the SelectStatement element O0801 via a link L0802 having max as a label.

  Finally, by generating a code from the inspection model 1008 shown in FIG. 17, the inspection code 0005 in the Promela language shown in FIG. 13 is generated.

  Next, a second example of conversion from the C language source code 0001 shown in FIG. 18 into the inspection code 0005 in the Promela language shown in FIG. 13 and the C language source code 0001 shown in FIG. 19 are shown in FIG. A third conversion example for conversion to the inspection code 0005 in the Promela language will be described with reference to FIGS. 18 and 19 are diagrams for explaining an example of C language source code 0001. FIG.

  The source code 0001 shown in FIGS. 18 and 19 is the same as the source code 0001 shown in FIG. 12 in that it is a program that executes a certain function do_something () with an arbitrary value from 1 to 50 as an argument. However, the source code 0001 shown in FIGS. 12, 18 and 19 has different methods for generating random numbers.

  In the source code 0001 shown in FIG. 18, the system function time () for returning the current time is set as a pseudo random number generation function, and 1 is added to the remainder obtained by dividing the return value of the random number generation function by 50. A random value of is generated.

  In the source code 0001 shown in FIG. 19, a random value of 1 to 50 is generated by adding 1 to the remainder of dividing the return value of the random number generation function my_rand () uniquely defined in lines 101 to 107 by 50. Is done. Here, the random number generation function my_rand () defined in the lines 101 to 107 receives the maximum value (50) and the minimum value (1) of the range of random numbers generated by itself as arguments, and the random number generation function my_rand ( ) Is obtained by subtracting the minimum value from the maximum value and adding 1 as the division value, and adding the minimum value to the remainder of dividing the return value of the function rand () that generates a random integer value by the division value. Generate random values from 1 to 50. Note that the range of random numbers generated by the random number generation function my_rand () is defined in line 0001.

  The programs indicated by the source code 0001 shown in FIGS. 18 and 19 are expressed by the implementation model 1205 shown in FIGS. 20 and 21, respectively.

  The implementation model 1205 shown in FIGS. 20 and 21 is converted into the generalization model 1206 shown in FIGS. 22 and 23 by the same implementation-generalization conversion rule 1005 as in the first conversion example.

  The generalization model 1206 shown in FIG. 22 is abstracted by the abstraction conversion rule 1006 and converted into the generalization model 1206 shown in FIG. The abstraction conversion rule 1006 used for the abstraction is obtained by converting the abstraction conversion rule 1006 used in the first conversion example so that the function time () is treated as a random number generation function like the function rand (). . That is, according to this abstraction conversion rule 1006, the BinaryOperation element O0501 of the generalization model 1206 shown in FIG. 22 and the element set that the BinaryOperation element O0501 has transitively are assigned to the logical element (Logical_Expression element O0701) shown in FIG. Converted.

  Similarly, the generalization model 1206 shown in FIG. 23 is abstracted by the abstraction conversion rule 1006 and converted into the generalization model 1206 shown in FIG. The abstraction conversion rule 1006 used for the abstraction is the same as the abstraction conversion rule 1006 used in the first conversion example, with the function my_rand (), the first argument as the minimum value, the second argument as the maximum value, and a random number. It has been changed to handle it as a function that occurs. That is, according to this abstraction conversion rule 1006, the FunctionCall element O0601 of the generalization model 1206 shown in FIG. 23 and the element set that the FunctionCall element O0601 transitively possesses are logical elements (Logical_Expression elements O0701) shown in FIG. Converted.

  The generalization model 1206 shown in FIG. 16 is converted into the inspection model 1207 shown in FIG. 17 by the same conversion rule as the generalization-inspection conversion rule 1007 used in the first conversion example. A test code 0005 in language is output.

  In the first to third conversion examples, the abstract conversion rule 1006 is changed to convert the different source code 0001 shown in FIGS. 12, 18 and 19 to the same inspection code 0005 shown in FIG. To do.

  In the present embodiment, an element that satisfies a predetermined condition is converted into a logical element in the process of abstracting the generalization model 1206 using the abstraction conversion rule 1006. As a result, as described in the second conversion example and the third conversion example, even if the input source code 0001 is changed, the administrator does not change all the conversion rules 1005 to 1007. By simply changing the abstraction conversion rule 1006, the source code 0001 can be changed and the same inspection code 0005 as before the change can be output.

  The fourth conversion example is a conversion example from the source code 0001 shown in FIG. 12 to the inspection code 0005 shown in FIG. 24 different from the inspection code 0005 shown in FIG.

  The inspection code 0005 shown in FIG. 24 will be described. In the inspection code 0005 shown in FIG. 13, a select statement is used as shown in the line 002. The select statement is a syntax added in SPIN version 6 or later, which is the inspection tool disclosed in Non-Patent Document 1, and if the inspection tool is a SPIN version 5 or earlier, the select statement cannot be used. Therefore, when the inspection tool is a version 5 or earlier SPIN, as shown in the line 101 to the line 116 in FIG. 24, by defining a syntax expressing non-deterministic execution in the inspection code 0005, it is equivalent to the select statement. It is necessary to express a simple process.

  In this conversion example, in order to convert the source code 0001 shown in FIG. 12 into the inspection code 0005 shown in FIG. 24, the source code 0001 shown in FIG. 12 is expressed by the mounting model 1205 shown in FIG. 15 is the same as the first conversion example, up to conversion to the generalization model 1206 shown in FIG. 15, abstracting the generalization model 1206, and converting it into the generalization model 1206 shown in FIG. A generalization-inspection conversion rule 1007 for converting the generalization model 1206 shown in FIG. 16 into an inspection model 1008 is different from the first conversion example.

  Specifically, in the generalization-check conversion rule 1007 of the fourth conversion example, the conversion destination element of the Logical_Expression element O0701 having “random value genaration” as the name of the abstracted generalization model 1206 shown in FIG. Is changed. By the generalization-inspection conversion rule 1007, the generalization model 1206 shown in FIG. 16 is converted into an inspection model 1008 shown in FIG.

  In the generalization-check conversion rule 1007 used in this conversion example, the logical_expression element O0701 of the abstracted generalization model 1206 shown in FIG. 16, the attribute element O0702 indicating the minimum value, and the attribute element O0703 indicating the maximum value are included. The combination is converted into a combination of elements O0901-0904 of the inspection model 1008 shown in FIG.

  Specifically, an InlineFunctionCall element O0905 of the inspection model 1008 illustrated in FIG. 25 includes an InlineFunctionDeclaration element O0901 referred to by a link L0901 having a declaration label, and a VariableReference element O0902 referred to by a link L0902 having an argument label indicating an argument. , An IntegerConstant element O0903 referred to by a link L0903 having an argument label, and an IntegerConstant element O0904 referred to by a link L0904 having an argument label are owned in this order. In FIG. 25, the inside of the declaration of the InlineFunctionDeclaration element O0901 is omitted, but the InlineFunctionDeclaration element O0901 takes a variable as the first argument, a minimum value as the second argument, and a maximum value as the third argument. Declared to have a program structure that implements a non-deterministic choice. A VariableReference element O0902 defines a variable to which a value is assigned. The IntegerConstant element O0903 is the minimum value. The IntegerConstant element O0904 is the maximum value.

  The inspection code 0005 shown in FIG. 24 can be acquired from the inspection model 1008 shown in FIG.

As described above, in the process of abstracting the generalization model 1206 using the abstraction conversion rule 1006, an element that meets a predetermined condition is converted into a logical element. As a result, even if the administrator desires to change the inspection code 0005 to be output, it is not necessary to change all the conversion rules 1005 to 1007, only the generalization-inspection conversion rule 1007 of the first conversion example. By changing, a desired inspection code can be output. Therefore, when using an inspection tool that is an SPIN of version 5 or earlier, it is possible to correspond to an SPIN of version 5 or earlier by changing only the generalization-inspection conversion rule 1007 of the first conversion example. If the generalization-inspection conversion rule 1007 among the conversion rules used in the conversion example 2 is changed to the generalization-inspection conversion rule 1007 used in the fourth conversion example, the source code 0001 shown in FIG. It is also possible to convert into the inspection code 0005 shown. Similarly, if the generalization-inspection conversion rule 1007 in the conversion rules used in the third conversion example is changed to the generalization-inspection conversion rule 1007 used in the fourth conversion example, the source shown in FIG. It is also possible to convert the code 0001 into the inspection code 0005 shown in FIG.

  Next, a fifth conversion example in which the abstraction process for the generalization model 1206 is executed a plurality of times and converted from a certain logical element to a different logical element will be described with reference to FIGS. In the fifth conversion example, the source code 0001 in the C language shown in FIG. 26 is converted into the inspection code 0005 in the Promela language shown in FIG.

  In the source code 0001 shown in FIG. 26, the do_something1 () function is executed when the remainder obtained by dividing the return value of the rand () function that generates a random number by 2 is 0, and when the remainder is other than 0, The do_something2 () function is executed. In other words, the source code 0001 illustrated in FIG. 26 indicates a program in which the do_something1 () function or the do_something2 () function is selected at random and the selected function is executed.

  The source code 0001 shown in FIG. 26 is expressed by a mounting model 1205 shown in FIG. Also, the mounting model 1205 shown in FIG. 28 is converted into a generalization model 1206 shown in FIG. 29 by the mounting-generalization conversion rule 1005.

  Next, the generalization model 1206 shown in FIG. 29 is abstracted by the same abstraction conversion rule 1006 as in the first conversion example, and converted into the generalization model 1206 shown in FIG. In this conversion, the BinaryOperation element O1101, FunctionCall element O1102, and FunctionDeclaration element shown in FIG. 29 corresponding to the call of the rand function and the calculation of the remainder obtained by dividing the return value of the rand function by 2 in the generalization model 1206 shown in FIG. The combination of O1103 and IntegerConstant element 1104 is converted into a combination of Logical_Expression element O1201, Attribute element O1202, and Attribute element O1203 in generalization model 1206 shown in FIG.

  Further, the generalization model 1206 shown in FIG. 30 is converted into the generalization model 1206 shown in FIG. 31 by an abstraction conversion rule 1006 different from the abstraction conversion rule 1006 used for conversion to the generalization model 1206 shown in FIG. Is done. The abstract conversion rule 1006 converts a selective executable statement in which a random value is substituted into a variable used in a conditional expression into a non-deterministic selective executable statement. In other words, the above-mentioned selective executable statement is converted into a logical element indicating a selective executable statement in which one of the two options is randomly selected.

  Specifically, the SelectionStatement element O1204 of the generalization model 1206 shown in FIG. 30 is converted into the Logical_SelectionStatement element O1301 of the generalization model 1206 shown in FIG. The reason for this will be described below.

  A VariableReference element O1206 of the generalization model 1206 shown in FIG. 30 represents a variable to which a Logical_Expression element O1201 whose name attribute value is “random value generation” is substituted. The VariableReference element O1206 is transitively connected to the SelectionItem element O1205 through the link L1201, and the SelectionItem element O1205 is owned by the SelectionStatement element O1204. For this reason, since the SelectionStatement element O1204 matches a selection execution statement in which a random number value is substituted into a variable used in the conditional expression, the SelectionStatement element O1204 is converted into a Logical_SelectionStatement element O1301 that is a logical element expressing a nondeterministic selective execution statement. .

  In addition, an element that is transitively connected by the link L1201 having the condition label from the SelectionItem element O1205 in the generalization model 1206 shown in FIG. 30 generates a random number in order to select the do_something1 () function or the do_something2 () function. This is an element for determining whether or not the remainder obtained by dividing the generated random number by 2 is 0. In the generalization model 1206 shown in FIG. 31, since the Logical_SelectionStatement element O1301 expressing a non-deterministic selective execution statement is defined, the above-described elements of the generalization model 1206 shown in FIG. 30 become unnecessary. For this reason, these elements are deleted.

  As described above, in this conversion example, the Abstraction process is executed a plurality of times, and the SectionStatement element O1204 including the Logical_Expression element O1201 that is the logical element converted by the first abstraction process is the second abstraction process. It is converted into a Logical_SelectionStatement element O1301 which is an element.

  The generalization model 1206 shown in FIG. 31 is converted into the inspection model 1008 shown in FIG. 32 by the generalization-inspection conversion rule 1007, and the inspection code 0005 shown in FIG. 27 is output.

  As described above, in the fifth conversion example, the abstraction process is executed a plurality of times, and a logical element converted in one abstraction process is further converted into a logical element in another abstraction process. The inspection code can be output, and it is possible to prevent the explosion of the state where the number of states to be inspected becomes a huge amount.

  Even when the fifth conversion example is changed to the source code 0001 using a random number generation method different from the source code 0001 shown in FIG. 26, the changed conversion example is the same as the first to fourth conversion examples. If only the conversion rule corresponding to the random number generation method is changed, the changed source code 0001 can be converted into the desired inspection code 0005 without converting other conversion rules.

  According to this embodiment, by possessing an interface for inputting a plurality of conversion rules divided into fine granularities, a change in the level of abstraction by a user can be easily realized by an operation for inputting the conversion rules. . That is, since the user can select a plurality of fine-grained conversion rules through the input interface, the user can easily select and change the level of abstraction as shown in FIGS. 8A and 8B according to the situation. Is possible.

  The source code conversion method has a procedure for converting a source code to be inspected into an inspection code described in an input language of a model checker using a plurality of conversion rules, and the conversion rule includes an implementation-generalization conversion rule and Are classified into abstract conversion rules and generalization-inspection conversion rules, and conversion is performed in stages. Accordingly, when following the design change of the source code to be inspected, only the conversion rule related to the change among the plurality of conversion rules may be changed, and the change can be minimized. In addition, the implementation model, the generalization model, and the inspection model are each defined in the meta model, and by adding constraints, it is possible to verify that the conversion result by the conversion rule is not illegal. Accordingly, it is possible to prevent an increase in the verification cost of the conversion rule, which is caused by realizing a series of processes for converting the source code to be inspected while abstracting it into the inspection code by combining the fine-grained conversion rules.

  In addition, by possessing an interface for inputting multiple conversion rules divided into fine granularities, users can select the conversion rule according to the property to be inspected and the inspection level when changing the level of abstraction.・ Easily realized by input operation. This solves the problem that it is difficult to change the level of abstraction. For example, if there is a specific defect that occurs only during repeated execution, it is not possible to detect the specific defect by removing the repetition, but it is still possible to detect a defect that does not include the cause of the repetition. In addition, the number of states can be greatly reduced.

  Furthermore, by accumulating and reusing model conversion rules in the database, it is possible to respond to design changes of the inspection target source code and application to other software at a low cost.

  In addition, in order to inspect with different inspection tools, when outputting in the inspection tool format, only the meta / inspection model and generalization-inspection conversion rules need to be created, and the creation part is kept to a minimum. . This can reduce the cost when inspecting with different model checkers.

  In addition, in the conversion rule used to convert the generalized model into the inspection model, instead of converting the generalized model directly into the inspection model or converting between physical elements on the generalization model, A conversion rule can be shared by converting to a logical element in the generalization model and then converting to a check model.

(Second embodiment)
The source code conversion apparatus and conversion processing method according to the second embodiment of the present invention will be described with reference to FIG. In this embodiment, following the inspection code output step S104 shown in FIG. 33, the process proceeds to the conversion rule input step S102, whereby the input source code 0001 is repeatedly converted using a different conversion rule set 0002. Procedures may be taken. Further, in an embodiment, following the inspection code output step S104, the process proceeds to the conversion rule input step S102, and all or a part of the already input conversion rule set 0002 and newly input in the conversion rule input step S102. The conversion rule set 0002 may be combined and used as the conversion rule set 0002.

  According to this embodiment, the interface for inputting a plurality of conversion rules divided into fine granularities is owned, the input source code and the conversion rule set used for conversion are stored, and the source code is converted into the conversion rule. Since conversion can be performed by exchanging a part of the set, it is possible to reduce the trouble of repeatedly converting the same source code, such as when generating a plurality of inspection codes having different abstractions.

(Third embodiment)
A source code conversion apparatus and conversion processing method according to the third embodiment of the present invention will be described with reference to FIG. In the present embodiment, there is a step of verifying the mounting model generated in the process of obtaining the inspection code from the source code, the generalization model, and the inspection model based on the constraint condition.

  A procedure for verifying the validity of conversion will be described in detail with reference to FIG.

  When a specific conversion rule has a precondition for the target model at the time of conversion, the precondition of the specific conversion rule may not be satisfied by the application of another conversion rule in the model to be converted. As described above, when model conversion is performed according to the specific conversion rule when the precondition is not satisfied, the model of the conversion result may be in an invalid state. In addition, even when an error is included in the conversion rule, the conversion result model may be in an invalid state.

  In this embodiment, the step of inputting the source code 0001 of the software and the first conversion for converting the mounting model 1205 having the source code information 1001 into an intermediate format (generalization model 1206) that is a format independent of a specific programming language. A step of inputting a rule, a step of inputting a second conversion rule for performing an abstraction process on the intermediate format, and a step of inputting a third conversion rule for converting from the intermediate format to an inspection model 1008 having inspection code information Analyzing the software source code 0001 and converting it into an implementation model 1205; converting the software source code 0001 into the intermediate generalized model 1206 using the first conversion rule; Software expressed in the intermediate format using conversion rules (A) abstracting, using the third conversion rule, converting the intermediate format into the inspection model 1008, and using the inspection model 1008, generating the inspection code 0005 described in the input language of the verification tool And a sufficiency verification step of verifying the model at each stage based on the first constraint condition 0300, the second constraint condition 0301, and the third constraint condition 0302, respectively.

  The sufficiency verification based on the first constraint condition 0300, the second constraint condition 0301, and the third constraint condition 0302 of the model at each stage is performed by, for example, a meta model using MOF disclosed in Non-Patent Document 2. Or by describing constraints on the model defined by the meta model by OCL disclosed in Non-Patent Document 4.

  According to the present embodiment, by using the meta model and the constraint condition, it is possible to guarantee the validity of the conversion due to the collision between the conversion rules or the failure of the conversion rule. In this model conversion, a model in a format defined by the meta model is generated. In addition, a constraint condition can be added, and the validity of the generated model can be verified with the constraint conditions 0300-00302.

  Although the invention made by the present inventor has been specifically described based on the embodiments, the present invention is not limited to the above-described embodiments, and various modifications can be made without departing from the scope of the invention. Needless to say.

  The present invention can be applied to a source code conversion method for converting a software source code into an inspection code described in an input language of a verification tool.

0001 source code 0002 conversion rule 0003 meta model 0004 writing model 0005 inspection code 0031 physical element definition 0032 logical element definition 1000 source code conversion device 1100 input unit 1200 conversion processing unit 1300 output unit 1400 storage unit 1500 control unit 2000 model inspection tool 3000 inspection result

Claims (13)

A source code conversion method executed by a source code conversion apparatus that converts a software source code into an inspection code written in an input language of a verification tool using a plurality of different conversion rules,
The plurality of different conversion rules are obtained by dividing a series of processes for converting and abstracting the source code into the inspection code and dividing it into fine granularity,
The conversion rule is:
A first conversion rule for converting the source code into an intermediate format that is independent of a specific programming language;
A second conversion rule that abstracts the converted intermediate format;
A third conversion rule for converting the abstracted intermediate form into the inspection code,
The method
Inputting the source code;
Receiving an input of at least one first conversion rule;
Receiving an input of at least one second conversion rule;
Receiving an input of at least one third conversion rule;
Converting the source code into the intermediate format using the input first conversion rule;
Abstracting the transformed intermediate form using the input second transformation rule;
Using the inputted third conversion rule to convert the abstracted intermediate form into the inspection code,
The intermediate format can represent not only a physical element that is equivalent to an element of the source code or the inspection code but also a logical element that is an element generated in the step of abstracting the converted intermediate format. A source code conversion method characterized by that. The source code conversion method according to claim 1,
The logical element includes a reference to the associated physical element and any information;
Abstracting the converted intermediate form includes adding additional attribute information by converting an element that matches a predetermined condition defined in the second conversion rule into the logical element;
The step of converting into the inspection code includes the step of converting the logical element into an element equivalent to the element of the inspection code. In the source code conversion method according to claim 1 or 2,
The step of abstracting the transformed intermediate form can be performed multiple times,
Source code conversion characterized in that a logical element generated in a step of abstracting the software at a certain time is converted into a new logical element in a step of abstracting the software at a later time than that time Method. In the source code conversion method according to any one of claims 1 to 3,
At least one of the first conversion rule, the second conversion rule, and the third conversion rule is selected from a plurality of conversion rules stored in the source code conversion device, whereby an input is made. A source code conversion method characterized by being accepted. In the source code conversion method according to any one of claims 1 to 4,
At least one of the first conversion rule, the second conversion rule, and the third conversion rule is accepted according to a user description, and the source code conversion method is characterized in that: A source code conversion method by a source code conversion device,
Entering the software source code;
Entering different transformation rules,
Converting the source code into an inspection code described in an input language of a verification tool using the plurality of different conversion rules,
At least some of the plurality of conversion rules are selected and input from among a plurality of conversion rules stored in the source code conversion device,
The plurality of different conversion rules include an implementation-generalization conversion rule for converting the source code into a generalization model having generalized program information that does not depend on a description language of the source code, and abstracting the generalization model An abstraction conversion rule to be converted, and a generalization-check conversion rule for converting the abstracted generalized model into the check code,
The step of converting the source code into the inspection code includes:
Converting the source code into the generalization model using the implementation-generalization conversion rules;
Abstracting the generalization model using the abstraction transformation rules;
Converting the abstracted generalized model into the inspection code using the generalization-inspection conversion rule,
In a series of steps of converting the pre-Symbol source code into the test code, the form of the model is information maintained internally is defined by the metamodel,
The model includes an implementation model having information corresponding to the source code, the generalization model, and an inspection model having information corresponding to the inspection code,
The implementation model is defined by the meta / implementation model that is its metamodel,
The generalization model is defined by a meta-generalization model that is a metamodel thereof,
The inspection model is defined by a meta-inspection model that is a meta model thereof,
Each of the metamodels holds a definition of a data structure and information on constraints between elements included in the data,
The meta-generalization model includes a definition of a first physical element that is an element equivalent to the element of the meta-implementation model, a definition of a second physical element that is an element equivalent to an element of the meta-inspection model, And a definition of a logical element that is an element generated in the step of abstracting the generalization model using the abstraction conversion rule. The source code conversion method according to claim 6,
In the meta / generalization model, the logical element defined in the meta / generalization model is defined to inherit the first physical element or the second physical element defined in the meta / generalization model. A source code conversion method characterized in that: The source code conversion method according to claim 6 or 7,
The logical element includes a reference to the associated physical element and any information;
Abstracting the generalized model includes providing additional attribute information by converting an element that matches a predetermined condition defined in the abstraction conversion rule into the logical element;
The step of converting the generalized model into the inspection code includes the step of converting the logical element into an element equivalent to the element of the inspection code. The source code conversion method according to any one of claims 6 to 8,
The step of converting the generalized model into the inspection code can be executed a plurality of times,
A logical element generated in a step of abstracting a generalization model of a certain time is converted into a new logical element in a step of abstracting the generalization model of the subsequent times. Source code conversion method. The source code conversion method according to any one of claims 6 to 9,
The information about the conversion rule includes only identification information indicating the conversion rule stored in the storage unit of the source code conversion device,
A source code conversion method, wherein an entity of the conversion rule is extracted from the storage unit using the identification information, and the actual condition of the extracted conversion rule is used for conversion. In the source code conversion method according to any one of claims 6 to 10,
Extracting or generating search conditions for the conversion rule from the input source code,
A source code conversion method, wherein a conversion rule that matches the search condition is acquired from a storage unit of a source code conversion device, and the acquired conversion rule is received as the conversion rule. The source code conversion method according to any one of claims 6 to 11,
A source code conversion method characterized in that a data structure and semantics of each intermediate model of the implementation model, the generalization model, and the inspection model are defined by a meta model that defines a syntax. Source code conversion apparatus comprising a processor and a storage area, the source code of the software, by using a different plurality of conversion rules, source code conversion program for executing processing for converting the test code written in the input language Verifier Because
The plurality of different conversion rules are obtained by dividing a series of processes for converting and abstracting the source code into the inspection code and dividing it into fine granularity,
The conversion rule is:
A first conversion rule for converting the source code into an intermediate format that is independent of a specific programming language;
A second conversion rule that abstracts the converted intermediate format;
A third conversion rule for converting the abstracted intermediate form into the inspection code,
The process is
Inputting the source code;
Receiving an input of at least one first conversion rule;
Receiving an input of at least one second conversion rule;
Receiving an input of at least one third conversion rule;
Converting the source code into the intermediate format using the input first conversion rule;
Abstracting the transformed intermediate form using the input second transformation rule;
Using the inputted third conversion rule to convert the abstracted intermediate form into the inspection code,
The intermediate format can represent not only a physical element that is equivalent to an element of the source code or the inspection code but also a logical element that is an element generated in the step of abstracting the converted intermediate format. A source code conversion program characterized by being.

Images