Title:
MODEL CHECKING DEVICE AND MODEL CHECKING METHOD
Document Type and Number:
Japanese Patent JP2023157310
Kind Code:
A
Abstract:
To efficiently perform model checking of an information processing system achieved by linking multiple services.SOLUTION: A model checking device stores a component composition definition in which the specifications of an orchestrator that links services are prescribed in a predetermined prescribed format, post-synthesis verification properties prescribing the requirements for the orchestrator specifications in the predetermined prescribed format, and a formal specification prescribing the specifications of multiple services in the predetermined prescribed format. Based on the post-synthesis verification properties, a partial specification extraction criteria is generated, which is a standard for extracting partial specifications, which are formal specifications of services used for validating orchestrator specifications. Based on the partial specification extraction criteria, the partial specification of the service used to verify the component composition definition is extracted from the formal specification of the service. Based on the extracted partial specifications, a verification code as a code for verifying the component composition definition is generated. The component composition definition is verified by inputting the verification code to a model checking tool.SELECTED DRAWING: Figure 5
More Like This:
| WO/2016/054426 | ERROR REPORT NORMALIZATION |
| WO/2022/177697 | CACHE-BASED TRACE LOGGING USING TAGS IN AN UPPER-LEVEL CACHE |
Inventors:
SHIMIZU RYO
KANUKA HIDEYUKI
TAKAHASHI HIROKI
KOGURE SHUNJI
NISHITANI JUNPEI
KANUKA HIDEYUKI
TAKAHASHI HIROKI
KOGURE SHUNJI
NISHITANI JUNPEI
Application Number:
JP2022067130A
Publication Date:
October 26, 2023
Filing Date:
April 14, 2022
Export Citation:
Assignee:
HITACHI LTD
International Classes:
G06F11/36
Attorney, Agent or Firm:
Patent Attorney Corporation Isshiki International Patent Office