JP7780382B2 - Model checking device and model checking method - Google Patents

Description

The present invention relates to a model checking device and a model checking method.

Patent Document 1 describes a program verification and generation device that verifies whether components satisfy the required specifications of a program. The program verification and generation device stores components that describe implementation and verification information for verifying operation, as well as program specifications that describe identification information for components required for a program and the specifications that the program must satisfy. It selects components based on the identification information in the program specifications, uses the verification information for the selected components to verify whether the selected components satisfy the program specifications, and, if it verifies that the selected components satisfy the program specifications, combines the implementation of the selected components using the program specifications to generate a program.

Patent Document 2 describes a combination service inspection system that, when developing a new service model by combining multiple previously developed service models, inspects whether the new service model is designed according to the required specifications. The system obtains an inspection code for inspecting a second service model from a database that records inspection codes for inspecting multiple previously developed first service models, obtains inspection conditions for the second service model, converts the obtained inspection conditions into inspection condition codes, and inspects whether the second service model meets the inspection conditions based on the obtained inspection codes and inspection condition codes.

Patent Document 3 describes an inspection device for a design model that describes software processing functions based on a specification model that describes product specifications. When inspecting a specification model represented by the transitions of multiple function blocks, the inspection device verifies whether each of the multiple function blocks satisfies its target value. If a function block with a state transition that does not satisfy the target value is extracted, the inspection device resets the target value to match the state transition, and resets the target values of other function blocks according to the target values of the specification model. Furthermore, if the other function blocks satisfy the reset target values under constraints that cause the extracted function block to violate the target value, the inspection device determines that the specification model satisfies the target value.

Japanese Patent Application Laid-Open No. 2004-326366 JP 2009-98770 A International Publication No. 2011/096037

In recent years, microservice architecture (MSA) has been gaining attention as a way to speed up the development of information processing systems. In MSA, information processing systems are developed as a combination of fine-grained, independently deployable services. This limits the scope of impact during maintenance and specification changes, enabling rapid releases and modifications.

In developing an information processing system using MSA, requests from users are processed as distributed processing that involves the coordination of multiple services. However, distributed processing must be designed to ensure requirements such as data consistency are met in the event of a failure in an individual service or communication, making the design more difficult than system development based on a monolithic architecture (monolith).

Model checking is a technology that supports the design of distributed processing systems, such as MSA-based information processing systems. It expresses the system from a specific perspective as a formal specification (hereafter referred to as "formal specification") and comprehensively verifies whether the formal specification satisfies given requirements (hereafter referred to as "verification properties").

When model checking an information processing system using MSA, the verification properties of the formal specifications of the services are first verified for each individual service. Next, the formal specifications of each service are synthesized to generate a formal specification for the orchestrator that connects the services, and the verification properties specific to the orchestrator are verified based on this formal specification.

However, when performing verification using the above method, formal specifications of components unrelated to the verification properties are included in the formal specifications of the synthesized orchestrator, which poses the problem of expanding the search space during verification and increasing verification time. Furthermore, if services are updated frequently, simply synthesizing all formal specifications after each update will result in the synthesized formal specifications including formal specifications unrelated to the orchestrator's verification properties, resulting in unnecessary re-synthesis and re-verification.

The program verification and generation device described in Patent Document 1 describes verification information and implementation for verifying operation in components, selects components based on identification information in the program specifications, and uses the verification information of the selected components to verify whether the verification information of the components satisfies the specifications of the program to be generated. However, this document does not describe a mechanism for preventing the search space from expanding during verification or for preventing unnecessary re-synthesis/re-verification.

Furthermore, the service inspection system described in Patent Document 2 obtains an inspection code for inspecting a second service model (a new service model) from a database that records inspection codes for multiple developed first service models, obtains inspection conditions for the second service model and converts them into inspection condition codes, and inspects whether the second service model meets the inspection conditions based on the inspection code and inspection condition codes. However, this document does not describe a mechanism for preventing the search space from expanding during verification or unnecessary re-synthesis/re-verification due to the reasons mentioned above.

Furthermore, the inspection device described in Patent Document 3 determines that a specification model satisfies a target value if other functional blocks satisfy the reset target value under constraints that cause an extracted functional block to violate the target value. However, this document does not describe a mechanism for preventing the search space from expanding during verification or unnecessary re-synthesis/re-verification due to the reasons mentioned above.

The present invention was made in light of this background, and aims to provide a model checking device and model checking method that can efficiently perform model checking of information processing systems realized by the collaboration of multiple services.

One aspect of the present invention to achieve the above object is a model checking device that performs model checking on an information processing system realized by the coordination of a plurality of services, the model checking device being configured using an information processing device having a processor and a storage device, and storing: a component synthesis definition in which a specification of an orchestrator that coordinates the services is described in a predetermined description format; a post-synthesis verification property in which requirements for the orchestrator specification are described in the predetermined description format; and a formal specification in which the specifications of each of the plurality of services are described in the predetermined description format; the device generates partial specification extraction criteria, which are information that serves as a standard for extracting partial specifications, which are formal specifications of the services to be used in verifying the orchestrator specification, based on the post-synthesis verification property; extracts the partial specifications of the services to be used in verifying the component synthesis definition from the formal specifications of the services based on the partial specification extraction criteria; generates verification code, which is code for verifying the component synthesis definition, based on the extracted partial specifications ; verifies the component synthesis definition by inputting the verification code into a model checking tool; and generates the partial specification extraction criteria based on variables or events used in describing logic in the post-synthesis verification property.

Furthermore, the problems disclosed in this application and the solutions thereto will be made clear in the detailed description and drawings.

This invention makes it possible to efficiently perform model checking of information processing systems that are realized through the collaboration of multiple services.

FIG. 10 is a diagram illustrating an example of model checking. FIG. 1 illustrates an example of model checking of an MSA-based model. FIG. 1 illustrates an example of model checking performed by a model checking device. FIG. 1 illustrates an example of model checking performed by a model checking device. FIG. 1 illustrates an example of model checking performed by a model checking device. FIG. 2 is a diagram illustrating an example of main functions of a model checking device. FIG. 2 is a system flow diagram illustrating an example of the function of the model checking device. 10 is a flowchart illustrating an example of a model checking process. 10 is a flowchart illustrating an example of a process for determining whether or not verification of an updated component is required; 10 is an example of a past extraction part specification. 10 is an example of a partial specification for synthesis. 10 is a flowchart illustrating an example of a partial specification extraction process for a non-updated part. 10 is a flowchart illustrating an example of a process for determining whether or not other model checking needs to be performed. FIG. 10 is a diagram illustrating an example of a process for determining whether or not other model checking needs to be performed. 1 is an example of an information processing device used in the configuration of a model checking device.

Embodiments of the present invention will be described in detail below, with reference to the accompanying drawings as appropriate. In the following description, various data may be described using terms such as "information" and "table," but the various data may be represented or managed using methods other than the data structures shown in the examples. Also, in the following description, the letter "S" before a reference number indicates a processing step.

The following describes a model checking device 100 according to one embodiment of the present invention. The model checking device 100 performs model checking on an information processing system (hereinafter referred to as a "model") derived from hardware and software designs, thereby verifying whether the system satisfies requirements from users, etc.

Model checking is a technique for verifying whether a model meets the requirements of users, etc. In model checking, the model design and requirements are described using a model description language, which is a language with rigorous mathematical meaning, and the specifications of the target model are comprehensively verified to see whether they meet the requirements.

Tools for model checking (hereinafter referred to as "model checking tools") include, for example, "TLA+" and "SPIN (Simple Promela INterpreter)," which are used to verify the design of distributed processing systems, such as the integration of services (microservices) in a cloud environment. Hereinafter, the model specifications written in a predetermined model description language will be referred to as "formal specifications," and requirements for a model from users, etc., written in a predetermined verification formula (logical formula) will be referred to as "verification properties."

Figure 1 is a diagram explaining model checking. As shown in the figure, in model checking, the model specifications are expressed as a formal specification 32 written in a specified model description language, and a comprehensive verification is performed to determine whether verification properties 31 are satisfied in a state space 33 that lists all possible states that the formal specification 32 can take.

When model checking a model based on microservice architecture (MSA), the verification properties of the formal specifications of each independently developed service are first verified individually. Next, the formal specifications of each service are synthesized based on the specifications of the orchestrator that connects the services (hereinafter referred to as the "component synthesis definition") to generate verification code (hereinafter referred to as the "synthesized verification code"), and it is verified whether the synthesized verification code satisfies the verification properties of the orchestrator specifications (hereinafter referred to as the "post-synthesis verification properties").

Figure 2 shows an example of model checking using "TLA+" for a model based on MSA. In this example, the model (the business realized by the orchestrator) is an information processing system that performs "transfer of funds between accounts." The post-composition verification property is "Eventually, the total balance of all accounts will match the total initial balance of the system (= no loss or increase of balance during the transaction process)." As shown as a component composition definition in the figure, the model shown in the example consists of two components: "Withdraw" and "Deposit."
In this example, the formal specifications of the service "Withdraw" and the service "Deposit" are obtained, and then the synthesized verification code is generated by synthesizing them.

In the example of Figure 2, the synthesized verification code is generated by simply combining the components (including formal specifications) of each service (hereinafter referred to as "software components"). As a result, software components (including formal specifications) that are unrelated to the post-synthesis verification property end up in the synthesized verification code, causing the verification target (hereinafter referred to as "search space") to expand. For example, if the model is "transfer of funds between accounts" and the post-synthesis verification property is "balance must not become negative," then although "recording transaction details" is unrelated to the post-synthesis verification property, the search space expands depending on the variables used in the transaction details and the values (number of states) that these variables can take.

Furthermore, when services are updated frequently, simply composing all formal specifications after each update may result in the composite formal specification including formal specifications unrelated to the orchestrator's verification properties, resulting in unnecessary re-composition and re-verification. For example, if the model is "Inter-account fund transfer" and the post-composition verification property is "Balance must not become negative," and a "Fee addition process" is added, re-verification is required because account balance manipulation is involved. However, if, for example, "Information to output details" is added and the "Retrieve past details" process is updated, re-composition and re-verification are unnecessary because they do not involve account balance manipulation, but re-composition and re-verification will still be required in this case.

Therefore, the model checking device 100 of this embodiment generates extraction criteria for formal specifications (hereinafter referred to as "partial specification extraction criteria") by focusing on information on verification properties (variables and events in logical expressions) that are specific to formal verification among the post-synthesis verification properties. Then, the model checking device 100 extracts formal specifications (hereinafter referred to as "partial specification extraction criteria") to be used for post-synthesis verification based on the partial specification extraction criteria from the formal specifications of each service.
By extracting partial specifications (called "partial specifications") and synthesizing the extracted partial specifications to generate synthesized verification code, the size of the synthesized verification code is reduced, thereby suppressing the expansion of the search space.

An example is shown in Fig. 3. In this example, the model checking device 100 generates a partial specification extraction criterion focusing on "variable: accounts, total" based on the post-synthesis verification property "EventuallyConsistentAccount == []<>(Sum(accounts) = total)". Furthermore, using the generated partial specification extraction criterion, the model checking device 100 extracts "Withdraw service" and "Deposit service" as partial specifications from the formal specifications of each service, and synthesizes them based on the component synthesis definition to generate synthesized verification code.

In addition, when a service is updated, the model checking device 100 re-extracts the partial specifications of the updated service, compares the re-extracted partial specifications with previously extracted partial specifications, and includes the re-extracted partial specifications in the synthesized verification code only if there is a difference between the two, thereby suppressing unnecessary verification when the service is updated.

Examples of this case are shown in Figures 4A and 4B. Figure 4A shows a case where, for an updated service "Withdraw service specification ver.2," there is no difference between the partial specification "Withdraw service ver.1 partial specification" extracted in the past (before the update) and the partial specification "Withdraw service ver.2 partial specification" extracted after the update. In this case, the model checking device 100 does not include the partial specification "Withdraw service ver.2 partial specification" extracted after the update in the synthesized verification code. On the other hand, Figure 4B shows a case where, for an updated service "Withdraw service specification ver.2," there is a difference between the partial specification "Withdraw service ver.1 partial specification" extracted in the past (before the update) and the partial specification "Withdraw service ver.2 partial specification" extracted after the update. In this case, the model checking device 100 includes the partial specification "Withdraw service ver.2 partial specification" extracted after the update in the synthesized verification code.

Furthermore, after re-extracting the partial specifications when a service is updated, if there are differences between the partial specifications before and after the update, the model checking device 100 notifies other component synthesis definitions that reference the partial specifications before the update that the partial specifications have been updated and that re-verification of those partial specifications is necessary, thereby preventing verification omissions.

<Detailed configuration>
Fig. 5 is a block diagram showing the main functions of model checking device 100, and Fig. 6 is a system flow diagram explaining the functions of model checking device 100. As shown in these figures, model checking device 100 has the following functions: storage unit 110, information acquisition management unit 130, updated component extraction unit 135, non-updated component extraction unit 140, partial specification extraction criterion generation unit 145, updated component verification necessity determination unit 150, non-updated component partial specification extraction unit 155, verification code generation unit 160, model checking execution unit 165, and other model checking execution necessity determination unit 170.

Of the above functions, the storage unit 110 stores the following information (data): component synthesis definition 111, post-synthesis verification properties 112, software component group 113, updated component group 114, non-updated component group 115, previously extracted partial specifications 118, partial specification extraction criteria 116, partial specifications for synthesis 117, synthesized verification code 119, and verification results 120.

Among these, the component composition definition 111 is the component composition definition described above, and includes a description of the formal specification of an orchestrator that realizes business by linking services. The component composition definition 111 also includes information (hereinafter referred to as "update presence/absence information") indicating whether software components developed independently for each service of a model to be subjected to model checking (hereinafter referred to as "target model") have been updated since the previous model checking. The component composition definition 111 also includes component composition definitions of the target model and models other than the target model.

Post-composition verification properties 112 are the post-composition verification properties mentioned above, and include a description of verification properties specific to the orchestrator.

Software component group 113 includes information about software components that realize services for the target model and models other than the target model (software entities (code, etc.), service format specifications before and after software component updates, etc.). Information about software components in software component group 113 is identified and managed by software component identifiers (hereinafter referred to as "component IDs").

The updated component group 114 includes information on software components that have been updated since the previous model checking, extracted from the software component group 113 by the updated component extraction unit 135.

The non-updated component group 115 includes information on software components that have not been updated since the previous model checking, extracted from the software component group 113 by the non-updated component extraction unit 140.

The partial specification extraction criteria 116 include criteria (extraction conditions; hereinafter referred to as "partial specification extraction criteria") used when extracting formal specifications (partial specifications) to be used in generating synthesized verification code from the updated component group 114 or the non-updated component group 115, which are generated by the partial specification extraction criteria generation unit 145 based on the post-synthesis verification properties 112.

The synthesis partial specifications 117 include partial specifications (hereinafter referred to as "synthesis partial specifications") that are extracted by the updated component verification necessity determination unit 150 or the non-updated component partial specification extraction unit 155 and that are used by the verification code generation unit 160 to generate the synthesized verification code 119.

The previously extracted partial specifications 118 include partial specifications (hereinafter referred to as "previously extracted partial specifications") previously extracted by the updated component verification necessity determination unit 150 or the non-updated component partial specification extraction unit 155.

The synthesized verification code 119 includes the synthesized verification code generated by the verification code generation unit 160 using the synthesis partial specification 117.

The verification result 120 includes information about the results of the model checking execution unit 165 verifying through model checking whether the synthesized verification code 119 satisfies the post-synthesis verification property 112.

The information acquisition and management unit 130 acquires various information required for model checking (component synthesis definition 111, post-synthesis verification properties 112, software component group 113, etc.) via a user interface, communication network, etc., and manages the acquired information in the storage unit 110.

The updated component extraction unit 135 identifies software components that have been updated since the previous model checking based on the update presence/absence information in the component synthesis definition 111, and extracts information (including formal specifications) of the identified software components from the software component group 113. The extracted information is stored in the storage unit 110 as the updated component group 114.

The no-update component extraction unit 140 identifies software components that have not been updated since the previous model checking, based on the update presence/absence information in the component synthesis definition 111, and extracts information (including formal specifications) of the identified software components from the software component group 113. The storage unit 110 stores the extracted information as the no-update component group 115.

The partial specification extraction criteria generation unit 145 generates partial specification extraction criteria based on the post-synthesis verification properties 112. The generated partial specification extraction criteria are stored in the storage unit 110 as partial specification extraction criteria 116.

The updated component verification necessity determination unit 150 extracts, as partial specifications, formal specifications to be used in generating synthesized verification code from the updated component group 114 based on the partial specification extraction criteria 116. The extracted partial specifications are stored in the storage unit 110 as synthesis partial specifications 117 and previously extracted partial specifications 118.

The non-updated component partial specification extraction unit 155 extracts formal specifications to be used in generating synthesized verification code as partial specifications from the non-updated component group 115 based on the partial specification extraction criteria 116. The extracted partial specifications are stored in the storage unit 110 as synthesis partial specifications 117 and previously extracted partial specifications 118.

The verification code generation unit 160 references the component synthesis definition 111 and generates synthesized verification code based on the synthesis partial specification 117. The generated synthesized verification code is stored in the storage unit 110 as synthesized verification code 119.

The model checking execution unit 165 performs model checking of the target model by providing the synthesized verification code 119 to a model checking tool, and outputs the results as verification results 120.

The other model checking execution necessity determination unit 170 acquires the pre-update partial specifications for software components whose partial specifications the updated component verification necessity determination unit 150 has determined require updating, and determines whether the acquired pre-update partial specifications are included in the component synthesis definition of other models other than the target model. If the determination result shows that the acquired pre-update partial specifications are included in the component synthesis definition of other models, the other model checking execution necessity determination unit 170 outputs information indicating that re-verification of the other models is required.

Figure 7 is a flowchart explaining the process (hereinafter referred to as "model checking process S700") performed by the model checking device 100 configured as described above when checking a target model. The model checking process S700 will be explained below with reference to this figure. Note that at the start of the model checking process S700, the storage unit 110 is assumed to store the information necessary for executing the model checking process S700 (component synthesis definition 111, post-synthesis verification property 122, software component group 113, etc.).

As shown in the figure, first, the updated component extraction unit 135 identifies software components that have been updated since the previous model checking based on the update presence/absence information in the component synthesis definition 111, and extracts information (including formal specifications) of the identified software components from the software component group 113. The extracted information is stored in the storage unit 110 as the updated component group 114 (S711).

Next, the no-update component extraction unit 140 identifies software components that have not been updated since the previous model checking based on the update/non-update information in the component synthesis definition 111, and extracts information (including formal specifications) of the identified software components from the software component group 113. The extracted information is stored in the storage unit 110 as the no-update component group 115 (S712).

Next, the partial specification extraction criterion generation unit 145 generates partial specification extraction criteria based on the post-synthesis verification property 112. The generated partial specification extraction criteria are stored in the storage unit 110 as partial specification extraction criteria 116 (S713).

Next, the updated component verification necessity determination unit 150 performs a process to extract partial specifications to be used in generating the synthesized verification code from the updated component group 114 based on the partial specification extraction criteria 116 (hereinafter referred to as the "updated component verification necessity determination process S714").

Figure 8 is a flowchart explaining the details of the verification necessity determination process S714 for updated parts. Below, we will explain the verification necessity determination process S714 for updated parts using this figure.

First, the updated component verification necessity determination unit 150 selects one software component from the updated component group 114 (S811).

Next, the updated component verification necessity determination unit 150 extracts partial specifications from the selected software components based on the partial specification extraction criteria 116 (S812).

Next, the updated component verification necessity determination unit 150 determines whether data exists in the previously extracted partial specifications 118 whose component ID (component ID 1181 described below) and partial specification extraction criteria (partial specification extraction criteria 1182 described below) match those of the currently selected software component (S813).

Figure 9 shows an example of a past extraction partial specification 118. As shown in the figure, the illustrated past extraction partial specification 118 is made up of one or more records having the following items: component ID 1181, partial specification extraction criteria 1182, and partial specification 1183. One record of the past extraction partial specification 118 corresponds to one partial specification. Of the above items, component ID 1181 stores the identifier of the software component (hereinafter referred to as "component ID"). Partial specification extraction criteria 1182 stores the partial specification extraction criteria used to extract the partial specification. Partial specification 1183 stores the content of the partial specification.

Returning to Figure 8, if data whose component ID and partial specification extraction criteria match those of the currently selected software component exists in the previously extracted partial specification 118 (S813: YES), processing proceeds to S814. On the other hand, if data whose component ID and partial specification extraction criteria match those of the currently selected software component does not exist in the previously extracted partial specification 118 (S813: NO), processing proceeds to S816.

In S814, the updated component verification necessity determination unit 150 determines whether there is a difference between the partial specification extracted in S812 and the partial specification of the previously extracted partial specification 118 that matched in S813. If there is no difference (S814: NO), processing proceeds to S815. On the other hand, if there is a difference (S814: YES), processing proceeds to S816.

In S815, the updated component verification necessity determination unit 150 stores the partial specification extracted in S812 in the partial specification for synthesis 117 as "verification not required." Processing then proceeds to S817.

Figure 10 shows an example of a partial specification for synthesis 117. As shown in the figure, the illustrated partial specification for synthesis 117 is composed of one or more records each having the following items: component synthesis definition 1171, partial specification 1172, and whether verification is required 1173. One record of the partial specification for synthesis 117 corresponds to one partial specification.

Of the above items, the component synthesis definition 1171 stores an identifier of the component synthesis definition (such as the name of the service). The partial specification 1172 stores a partial specification. The verification necessity 1173 stores information indicating whether or not the partial specification needs to be verified ("verification necessary" or "verification not necessary").

Returning to FIG. 8 , in S816, the updated component verification necessity determination unit 150 stores the partial specification extracted in S812 as "verification required" in the partial specification for synthesis 117. The updated component verification necessity determination unit 150 also stores the partial specification in the previously extracted partial specification 118. Processing then proceeds to S817.

In S817, the updated component verification necessity determination unit 150 determines whether all software components in the updated component group 114 have been selected in S811. If the updated component verification necessity determination unit 150 determines that not all software components have been selected (S817: NO), processing returns to S811. On the other hand, if the updated component verification necessity determination unit 150 determines that all software components have been selected (S817: YES), the updated component verification necessity determination process S714 ends and processing proceeds to S715 in Figure 7.

Returning to FIG. 7 , in S715, the model checking device 100 determines whether or not a record exists in which "verification required" is stored in the verification necessity 1173 of the partial specification for synthesis 117. If a record in which "verification required" is stored in the verification necessity 1173 of the partial specification for synthesis 117 exists (S715: YES), the model checking device 100 executes a process of extracting partial specifications from the non-updated component group 115 (hereinafter referred to as "non-updated component partial specification extraction process S716"). On the other hand, if a record in which "verification required" is stored in the verification necessity 1173 of the partial specification for synthesis 117 exists (S715: NO), the model checking process S700 ends.

Figure 11 is a flowchart explaining the details of the partial specification extraction process S716 for non-updated parts. Below, we will explain the partial specification extraction process S716 for non-updated parts using this figure.

First, the non-updated component partial specification extraction unit 155 selects one software component from the non-updated component group 115 (S1111).

Next, the non-updated component partial specification extraction unit 155 determines whether data whose component ID and partial specification extraction criteria match those of the currently selected software component exists in the previously extracted component specification 118 (S1112). If the non-updated component partial specification extraction unit 155 determines that data whose component ID and partial specification extraction criteria match those of the currently selected software component exists in the previously extracted component specification 118 (S1112: YES), processing proceeds to S1113. On the other hand, if the non-updated component partial specification extraction unit 155 determines that data whose component ID and partial specification extraction criteria 116 match those of the currently selected software component does not exist in the previously extracted component specification 118 (S1112: NO), processing proceeds to S1114.

In S1113, the non-updated component partial specification extraction unit 155 stores the partial specifications of the data in the previously extracted partial specifications 118 that matched in S1112 as "no verification required" in the partial specifications for synthesis 117. Processing then proceeds to S1116.

In S1114, the non-updated component partial specification extraction unit 155 extracts partial specifications from the software components selected in S1111 based on the partial specification extraction criteria 116.

Next, the non-updated component partial specification extraction unit 155 stores the partial specification of the selected software component extracted in S1114 in the partial specification for synthesis 117 as "verification required." The non-updated component partial specification extraction unit 155 also stores this partial specification in the previously extracted partial specification 118 (S1115). Processing then proceeds to S1116.

In S1116, the non-updated component partial specification extraction unit 155 determines whether all software components in the non-updated component group 115 have been selected in S1111. If the updated component verification necessity determination unit 150 determines that all software components have not been selected (S1116: NO), processing returns to S1111. On the other hand, if the updated component verification necessity determination unit 150 determines that all software components have been selected (S1116: YES), the non-updated component partial specification extraction process S716 ends, and processing proceeds to S717 in Figure 7.

Returning to FIG. 7 , the verification code generation unit 160 then references the component synthesis definition 111 and generates synthesized verification code 119 based on the synthesis partial specification 117 (S717). The verification code generation unit 160 generates synthesized verification code 119 so that all partial specifications stored in the synthesis partial specification 117 will be subject to model checking by a model checking tool. That is, if there is even one partial specification in which "Verification required" is stored in the verification necessity 1173 of the synthesis partial specification 117 (S715: YES), the verification code generation unit 160 generates synthesized verification code 119 so that all partial specifications stored in the synthesis partial specification 117 (all partial specifications regardless of the content of verification necessity 1173) will be subject to model checking by a model checking tool (S717).

Next, the model checking execution unit 165 performs model checking of the target model by inputting the synthesized verification code 119 into a model checking tool, and outputs the results as verification results 120 (S718). The contents of the verification results 120 are provided to the user, for example, via a user interface.

Next, the other model checking execution necessity determination unit 170 executes a process to determine whether re-verification of other models is necessary (hereinafter referred to as the "other model checking execution necessity determination process S719").

Figure 12 is a flowchart explaining the details of the other model testing execution necessity determination process S719. Figure 13 is a diagram showing an example of the other model testing execution necessity determination process S719. Below, we will explain the other model testing execution necessity determination process S719 using these figures.

First, the other model checking execution necessity determination unit 170 selects one partial specification from the synthesis partial specification 117 that the updated component verification necessity determination unit 150 has determined to be "verification required" (a partial specification for which "verification required" is stored in verification necessity 1173) (S1211 in Figure 12).

Next, the other model checking execution necessity determination unit 170 obtains the pre-update partial specifications for the software components of the selected partial specification from the previously extracted partial specifications 118 (S1212 in Figure 12, S1311 in Figure 13).

Next, the other model checking execution necessity determination unit 170 references the component synthesis definition 111 and determines whether the acquired pre-update partial specification is included in the component synthesis definition of a model other than the target model (S1213 in FIG. 12, S1312 in FIG. 13). If the acquired pre-update partial specification is not included in the component synthesis definition of a model other than the target model (S1213 in FIG. 12: NO), processing proceeds to S1215. On the other hand, if the acquired pre-update partial specification is included in the component synthesis definition of a model other than the target model (S1213 in FIG. 12: YES), the other model checking execution necessity determination unit 170 outputs (e.g., presents to the user via a user interface) information indicating that re-verification of the other model is required (S1214 in FIG. 12, S1313 in FIG. 13).

In S1215, the other model checking execution necessity determination unit 170 determines whether all partial specifications set to require verification have been selected from the partial specifications to be synthesized 117. If the other model checking execution necessity determination unit 170 determines that there are partial specifications that have not been selected from the partial specifications to be synthesized 117 (S1215: NO), the processing returns to S1211. On the other hand, if the other model checking execution necessity determination unit 170 determines that all partial specifications set to require verification have been selected from the partial specifications to be synthesized 117 (S1215: YES), the processing returns to FIG. 7, and the model checking processing S700 ends.

As explained above, the model checking device 100 of this embodiment generates partial specification extraction criteria by focusing on information about verification properties specific to formal verification (variables and events in logical expressions) among the post-synthesis verification properties, extracts partial specifications, which are formal specifications to be used for post-synthesis verification, from the formal specifications of each service based on the partial specification extraction criteria, and synthesizes the extracted partial specifications to generate synthesized verification code. This reduces the size of the synthesized verification code and prevents the search space from expanding.

Furthermore, when a service is updated, the model checking device 100 re-extracts the partial specifications of the updated service, compares the re-extracted partial specifications with previously extracted partial specifications, and generates and verifies synthesized verification code only if there are differences between the two. Specifically, if the previously extracted partial specifications do not contain a partial specification that matches the updated partial specification of the service to be updated (updated component) (S816 in FIG. 8), or if the previously extracted partial specifications do not contain a partial specification of a service not to be updated (non-updated component) (S1115 in FIG. 11), that is, if the partial specifications to be synthesized contain at least one partial specification that "requires verification" (S715: YES), the model checking device 100 generates synthesized verification code (S717) and verifies the component synthesis definition (S718). On the other hand, if the previously extracted partial specifications contain a partial specification that matches the updated partial specification of the service (updated component) that is the target of the update (S815 in FIG. 8), and if the previously extracted partial specifications contain a partial specification of a software component that is not the target of the update (non-updated component) (S1113 in FIG. 11), that is, if the partial specifications to be synthesized do not contain any partial specifications that are marked as "verification required" (S715: NO), the model checking device 100 does not generate synthesized verification code or verify the component synthesis definition. Therefore, when a service is updated, if the partial specifications to be synthesized do not contain any partial specifications that are marked as "verification required," it is possible to prevent unnecessary re-synthesis and re-verification.

Furthermore, after re-extracting the partial specifications when a service is updated, if there is a difference between the partial specifications before and after the update, i.e., if there is even one partial specification that is deemed to "require verification" in the partial specifications for synthesis (S715: YES), the model checking device 100 notifies other component synthesis definitions that reference the partial specifications before the update that the partial specifications have been updated and that re-verification of those partial specifications is required (S719), thereby reliably preventing verification omissions.

In this way, the model checking device 100 of this embodiment can efficiently perform model checking of an information processing system that is realized by the collaboration of multiple services.

FIG. 14 shows an example of the configuration of an information processing device constituting a model checking device 100. The illustrated information processing device 10 includes a processor 11, a main memory device 12, an auxiliary memory device 13, an input device 14, an output device 15, and a communication device 16. Note that all or part of the illustrated information processing device 10 may be realized using virtual information processing resources provided using virtualization technology, process space separation technology, or the like, such as a virtual server provided by a cloud system. Furthermore, all or part of the functions provided by the information processing device 10 may be realized by a service provided by the cloud system via an API (Application Program Interface), for example. Furthermore, the model checking device 100 may be configured using multiple information processing devices 10 connected to each other so as to be able to communicate with each other.

In the figure, the processor 11 is, for example, a CPU (Central Processing Unit),
PU (Micro Processing Unit), GPU (Graphics Processing Unit), FPGA (Field Programmable Gate Array), ASIC (Application Specific Integrated Circuit)
), AI (Artificial Intelligence) chips, etc.

The main memory device 12 is a device for storing programs and data, and is, for example, a ROM (Read Only Memory).
Only Memory), RAM (Random Access Memory), and NVRAM (Non Volatile RAM).

The auxiliary storage device 13 is, for example, a solid state drive (SSD), a hard disk drive, an optical storage device (such as a compact disc (CD) or a digital versatile disc (DVD)), a storage system, an IC card, a read/write device for a recording medium such as an SD card or an optical recording medium, a storage area of a cloud server, etc. Programs and data can be read into the auxiliary storage device 13 via a recording medium reader or a communication device 16. The programs and data stored in the auxiliary storage device 13 are read into the main storage device 12 as needed.

The input device 14 is an interface that accepts input from outside, and may be, for example, a keyboard, mouse, touch panel, card reader, pen-input tablet, or voice input device.

The output device 15 is an interface that outputs various information such as processing progress and results. The output device 15 is, for example, a display device (liquid crystal monitor, LCD (Liquid Crystal Display), graphics card, etc.) that visualizes the various information described above, a device that converts the various information described above into audio (audio output device (speaker, etc.)), or a device that converts the various information described above into text (printer, etc.). Note that the information processing device 10 may also be configured to input and output information to and from other devices via the communication device 16, for example.

The input device 14 and output device 15 form a user interface that accepts and presents information to the user.

The communication device 16 is a device that enables communication with other devices. The communication device 16 is a wired or wireless communication interface that enables communication with other devices via a communication medium such as a communication network, and is, for example, a NIC (Network Interface Card), a wireless communication module, a USB module, etc.

The information processing device 10 may be equipped with, for example, an operating system, a file system, a DBMS (DataBase Management System) (relational database, NoSQL, etc.), a KVS (Key-Value Store), etc.

Each function of the model checking device 100 is realized by the processor 11 reading and executing a program stored in the main memory device 12, or by the hardware (FPGA, ASIC, AI chip, etc.) that constitutes the model checking device 100. The model checking device 100 stores the various pieces of information (data) described above, for example, as database tables or files managed by a file system.

Although one embodiment of the present invention has been described above, it goes without saying that the present invention is not limited to the above embodiment and can be modified in various ways without departing from the spirit of the present invention. For example, the above embodiment has been described in detail to clearly explain the present invention, and the present invention is not necessarily limited to an embodiment having all of the described configurations. Furthermore, it is possible to add, delete, or replace part of the configuration of the above embodiment with other configurations.

For example, the information extracted or generated in each step of the model checking process S700 shown in FIG. 7 (model configuration, service formal specification, component synthesis definition, post-synthesis verification properties, software component group, updated component group, non-updated component group, partial specification extraction criteria, partial specifications for synthesis, previously extracted partial specifications, synthesized verification code, verification results, etc.) may be presented on a user interface, allowing the user to visually grasp the process of the model checking process S700. Furthermore, at each step, editing of the various pieces of information described above may be accepted from the user via the user interface.

Furthermore, the above-mentioned configurations, functional units, processing units, processing means, etc. may be partly or entirely implemented in hardware by, for example, designing them as integrated circuits. The above-mentioned configurations, functions, etc. may also be implemented in software by a processor interpreting and executing a program that implements each function. Information such as the programs, tables, and files that implement each function can be stored in a memory, a hard disk, a recording device such as an SSD (Solid State Drive), an I/O device, etc.
It can be placed on a recording medium such as a C card, an SD card, or a DVD.

Furthermore, the layout of the various functional units, processing units, and databases of each information processing device described above is merely an example. The layout of the various functional units, processing units, and databases can be changed to an optimal layout in terms of the performance, processing efficiency, communication efficiency, etc. of the hardware and software equipped in these devices.

In addition, the structure (schema, etc.) of the database that stores the various types of data mentioned above can be flexibly changed from the perspective of efficient resource utilization, improved processing efficiency, improved access efficiency, improved search efficiency, etc.

100 Model checking device, 110 Storage unit, 111 Component synthesis definition, 112 Post-synthesis verification properties, 113 Software component group, 114 Updated component group, 115 Non-updated component group, 116 Partial specification extraction criteria, 117 Partial specifications for synthesis, 118 Previously extracted partial specifications, 119 Synthesized verification code, 120 Verification results, 130 Information acquisition and management unit, 135 Updated component extraction unit, 140 Non-updated component extraction unit, 145 Partial specification extraction criteria generation unit, 150 Updated component verification necessity determination unit, 155 Non-updated component partial specification extraction unit, 160 Verification code generation unit, 165 Model checking execution unit, 170 Other model checking execution necessity determination unit

Claims (8)

A model checking device that performs model checking on an information processing system realized by cooperation of a plurality of services,
The information processing device includes a processor and a storage device,
a component composition definition in which the specifications of an orchestrator that links the services are described in a predetermined description format;
a post-synthesis verification property in which requirements for the orchestrator specification are described in a predetermined description format;
a formal specification in which the specifications of each of the plurality of services are described in a predetermined description format;
Remember,
generating partial specification extraction criteria, which are information serving as criteria for extracting partial specifications, which are formal specifications of the service, to be used in verifying the orchestrator specification, based on the post-synthesis verification properties;
extracting the partial specification of the service to be used for verifying the component composition definition from the formal specification of the service based on the partial specification extraction criteria;
generating a verification code that is a code for verifying the component synthesis definition based on the extracted partial specification;
verifying the component synthesis definition by inputting the verification code into a model checking tool ;
generating the partial specification extraction criteria based on variables or events used in describing logic in the post-synthesis verification properties ;
Model checking equipment. A model checking device that performs model checking on an information processing system realized by cooperation of a plurality of services,
The information processing device includes a processor and a storage device,
a component composition definition in which the specifications of an orchestrator that links the services are described in a predetermined description format;
a post-synthesis verification property in which requirements for the orchestrator specification are described in a predetermined description format;
a formal specification in which the specifications of each of the plurality of services are described in a predetermined description format;
Remember,
generating partial specification extraction criteria, which are information serving as criteria for extracting partial specifications, which are formal specifications of the service, to be used in verifying the orchestrator specification, based on the post-synthesis verification properties;
extracting the partial specification of the service to be used for verifying the component composition definition from the formal specification of the service based on the partial specification extraction criteria;
generating a verification code that is a code for verifying the component synthesis definition based on the extracted partial specification;
verifying the component synthesis definition by inputting the verification code into a model checking tool ;
storing the partial specifications previously extracted from the formal specification of the service based on the partial specification extraction criteria as previously extracted partial specifications;
When the service is updated, extracting the updated partial specifications of the service that has been updated and the partial specifications of the service that has not been updated based on the partial specification extraction criteria;
If the partial specification that matches the updated partial specification of the service that has been updated does not exist in the past extracted partial specification, or if the partial specification of the service that has not been updated does not exist in the past extracted partial specification, generate the verification code and perform the verification of the component synthesis definition;
If the partial specification that matches the updated partial specification of the service that has been updated exists in the past extracted partial specification, and if the partial specification of the service that has not been updated exists in the past extracted partial specification, the verification code is not generated and the verification of the component composition definition is not performed.
Model checking equipment. 3. The model checking apparatus according to claim 2 ,
A plurality of component composition definitions each having a different orchestrator;
the partial specifications extracted for the plurality of component synthesis definitions based on the partial specification extraction criteria;
Remember,
If the partial specification that matches the updated partial specification of the service that has been updated does not exist in the past extracted partial specification, or if the partial specification of the service that has not been updated does not exist in the past extracted partial specification, extracting another component synthesis definition that includes the partial specification of the service before the update,
outputting information indicating that re-verification is required for the extracted other component synthesis definitions;
Model checking equipment. 2. The model checking apparatus according to claim 1,
The information processing system is configured using a microservice architecture (MSA), and the service is a microservice.
Model checking equipment. 2. The model checking apparatus according to claim 1,
a user interface that presents to a user at least one of the information on the model to be inspected, the formal specification of the service, the component synthesis definition, the post-synthesis verification property, the partial specification extraction criteria, the partial specifications, the verification code, and the verification result of the component synthesis definition, or that accepts editing of the information;
Model checking equipment. A model checking device configured using an information processing device having a processor and a storage device, which performs model checking on an information processing system realized by the cooperation of a plurality of services,
a component composition definition in which the specifications of an orchestrator that links the services are described in a predetermined description format;
a post-synthesis verification property in which requirements for the orchestrator specification are described in a predetermined description format;
a formal specification in which the specifications of each of the plurality of services are described in a predetermined description format;
storing the
generating partial specification extraction criteria, which are information serving as criteria for extracting partial specifications, which are formal specifications of the service used in verifying the orchestrator specification, based on the post-synthesis verification properties;
extracting the partial specification of the service to be used for verifying the component composition definition from the formal specification of the service based on the partial specification extraction criterion;
generating a verification code that is a code for verifying the component synthesis definition based on the extracted partial specifications ;
verifying the component synthesis definition by inputting the verification code into a model checking tool; and
generating the partial specification extraction criteria based on variables or events used in describing logic in the post-synthesis verification properties;
,Model checking method. A model checking device configured using an information processing device having a processor and a storage device, which performs model checking on an information processing system realized by the cooperation of a plurality of services,
a component composition definition in which the specifications of an orchestrator that links the services are described in a predetermined description format;
a post-synthesis verification property in which requirements for the orchestrator specification are described in a predetermined description format;
a formal specification in which the specifications of each of the plurality of services are described in a predetermined description format;
storing the
generating partial specification extraction criteria, which are information serving as criteria for extracting partial specifications, which are formal specifications of the service used in verifying the orchestrator specification, based on the post-synthesis verification properties;
extracting the partial specification of the service to be used for verifying the component composition definition from the formal specification of the service based on the partial specification extraction criterion;
generating a verification code that is a code for verifying the component synthesis definition based on the extracted partial specifications ;
verifying the component synthesis definition by inputting the verification code into a model checking tool;
a step of storing the partial specifications previously extracted from the formal specification of the service based on the partial specification extraction criteria as previously extracted partial specifications;
When the service is updated, extracting the updated partial specifications of the service that has been updated and the partial specifications of the service that has not been updated based on the partial specification extraction criteria;
The partial specification that matches the updated partial specification of the service that is the target of the update
does not exist in the past extracted partial specification, or if the partial specification of the service that is not the target of the update does not exist in the past extracted partial specification, generating the verification code and verifying the component synthesis definition; and
a step of not generating the verification code and not performing the verification of the component composition definition when the partial specification that matches the updated partial specification of the service that has become the target of the update exists in the past extracted partial specification and the partial specification of the service that has not become the target of the update exists in the past extracted partial specification;
, Model checking method. 8. A model checking method according to claim 7 ,
The model checking apparatus
A plurality of component composition definitions each having a different orchestrator;
the partial specifications extracted for the plurality of component synthesis definitions based on the partial specification extraction criteria;
storing the
extracting another component synthesis definition including a partial specification of the service before the update when the partial specification that matches the partial specification of the service after the update does not exist in the past extracted partial specification, or when the partial specification of the service that is not the target of the update does not exist in the past extracted partial specification; and
a step of outputting information indicating that reverification is required for the extracted other component synthesis definitions;
Further, the model checking method performs the above.