JP7799643B2 - Specification verification support device, method, and program - Google Patents

Description

This disclosure relates to technology for verifying system specifications for information systems.

When developing an information system, the developer listens to the requirements of the client procuring the information system and writes them down as system specifications. The client and developer then confirm the system specifications, and the information system is then designed and created in accordance with the specifications. Since errors in the system specifications can cause malfunctions in the information system, verifying the system specifications is important in system development.

State transition models are sometimes used to describe system specifications. A state transition model is a model that represents, for each object that makes up an information system, the states that the object can take, the events that occur to the object, and the state transitions caused by the events. A state transition model is described as a state transition diagram or state transition table.

Patent Document 1 discloses a device for editing a state transition table. The state transition table editing device in Patent Document 1 allows a system verifier to specify simplification of state transition specifications based on a sequence diagram, enabling the verifier to correctly simplify the state transition specifications. The state transition table editing device displays a sequence diagram and prompts the verifier to input a state transition table reduction perspective and the portion of the sequence diagram to be reduced. Based on the input state transition table reduction perspective and the portion of the sequence diagram to be reduced, the device determines the reduction content of the state transition table and generates data for the reduced state transition table from data representing the original state transition table.

JP 2010-250422 A

According to the disclosure of Patent Document 1, system verification can be supported by simplifying the state transition table based on the perspective specified by the verifier. However, objects whose state transition models are shown in the system specifications are managed as individual, independent entities. Therefore, as the number of objects and their states increases, errors inherent in the system specifications, such as missing states or transitions, or inconsistencies between states, may be overlooked.

One objective of this disclosure is to provide technology that enables the reduction of overlooked errors in verifying system specifications.

One aspect of the specification verification support device included in the present disclosure is a specification verification support device that supports specification verification of an information system, and includes a specification registration unit that accepts registration of state transition specifications that specify state transitions due to events in each of multiple models, where the events include events that occur in other models due to state transitions of the models, and event constraints that specify violations that should be considered when the events occur, and a specification verification unit that verifies whether any events that correspond to the violations have occurred in the state transition specifications.

One aspect of the specification verification support method included in the present disclosure is a specification verification support method for supporting specification verification of an information system, in which a device equipped with a processor and memory accepts registration of state transition specifications that specify state transitions due to events in each of a plurality of models, where the events include events that occur in other models due to the state transitions of the models, and event constraints that specify violations that should be considered when the events occur, and verifies whether any events that correspond to the violations have occurred in the state transition specifications.

One aspect of the specification verification support program included in the present disclosure is a specification verification support program that supports specification verification of an information system, and causes a device equipped with a processor and memory to accept registration of state transition specifications that specify state transitions due to events in each of a plurality of models, where the events include events that occur in other models due to the state transition of one model, and event constraints that specify violations that should be considered when the event occurs, and to verify whether any events that correspond to the violations have occurred in the state transition specifications.

One aspect of the present disclosure makes it possible to reduce the chance of overlooking violations during verification of system specifications.

FIG. 1 is a conceptual diagram illustrating an example of a hardware configuration of a specification verification support device according to at least one embodiment of the present disclosure. FIG. 1 is a conceptual diagram illustrating an internal structure of formulated specification data according to at least one embodiment of the present disclosure. 1 is a flowchart illustrating a system specification determination process, according to at least one embodiment of the present disclosure. FIG. 1 is a conceptual diagram illustrating a format of formalized specification data according to at least one embodiment of the present disclosure. 10 is a flowchart illustrating a system specification registration process according to at least one embodiment of the present disclosure. 10 is a flowchart illustrating a system specification registration process according to at least one embodiment of the present disclosure. 10 is a flowchart illustrating an example of an event registration (standard) process according to at least one embodiment of the present disclosure. FIG. 10 is a diagram illustrating a processing example of an event registration (standard) process according to at least one of the embodiments of the present disclosure. 10 is a flowchart illustrating an event registration (exception) process according to at least one embodiment of the present disclosure. FIG. 10 is a diagram illustrating a processing example of an event registration (exception) process according to at least one of the embodiments of the present disclosure. 10 is a flowchart illustrating an event registration (sub-event) process according to at least one embodiment of the present disclosure. FIG. 10 is a diagram illustrating a processing example of an event registration (sub-event) process according to at least one of the embodiments of the present disclosure. 10 is a flowchart illustrating an example of an event registration (procedure result) process according to at least one embodiment of the present disclosure. FIG. 10 is a diagram illustrating a processing example of an event registration (procedure result) process according to at least one of the embodiments of the present disclosure. 10 is a flowchart illustrating a constraint registration process according to at least one embodiment of the present disclosure. 1 is a flowchart illustrating a system validation process according to at least one embodiment of the present disclosure. FIG. 10 is a conceptual diagram illustrating a format of specification verification result data according to at least one of the embodiments of the present disclosure. 10 is a flowchart illustrating a system comparison verification process according to at least one embodiment of the present disclosure. FIG. 10 is a conceptual diagram illustrating a format of specification comparison result data according to at least one embodiment of the present disclosure.

Embodiments of the present invention will be described below with reference to the drawings. Note that the examples described below do not limit the invention as defined in the claims. Furthermore, not all of the elements and combinations thereof described in the examples are necessarily essential to the solution of the invention.

Figure 1 is a conceptual diagram showing an example hardware configuration of a specification verification support device corresponding to at least one embodiment of the present disclosure.

The specification verification support device 1 includes a processor and memory (not shown).

The processor may be composed of, for example, a CPU (Central Processing Unit), MPU (Micro Processing Unit), GPU (Graphics Processing Unit), FPGA (Field-Programmable Gate Array), etc.

Memory is a device that stores programs and data, and includes, for example, Random Access Memory (RAM), Read Only Memory (ROM), and non-volatile semiconductor memory (Non-Volatile RAM (NVRAM)).

The memory may be, for example, a device for reading and writing data from and to recording media such as a hard disc drive (HDD), solid state drive (SSD), storage system, integrated circuit (IC) card, secure digital (SD) memory card, or optical recording media (compact disc (CD), digital versatile disc (DVD), etc.).

The processor reads and executes various programs, such as the specification verification support program, stored in memory to implement the data management unit 10, specification registration unit 20, specification verification unit 30, and specification comparison unit 40.

The data management unit 10 manages the system specification 110, specification verification result data 120, and specification comparison result data 130, which are data stored in the memory of the specification verification support device 1 or in a storage device of an external device seen from the specification verification support device 1.

The system specification 110 includes formalized specification data corresponding to one or more information systems. Formalized specification data refers to data related to the specifications of an information system that has been formulated as a single data structure in accordance with predetermined standards. Data related to the specifications of an information system refers to, for example, data in natural language format or UML format, but is not limited to data in these formats. In the illustrated example, the system specification 110 includes formalized specification data 111 for system 1 and formalized specification data 112 for system 2. The system specification 110 may similarly include formalized specification data for other systems.

The specification registration unit 20 accepts registration of state transition specifications 111A that specify state transitions due to events for each of multiple models, where the events include events that occur in other models due to state transitions of the model, and event constraints 111B that specify violations that should be considered when an event occurs.

In other words, the state transition specification 111A and event constraint 111B are data registered by the specification registration unit 20.

The specification verification unit 30 verifies whether any events that violate the state transition specification 111A have occurred.

That is, the specification verification unit 30 acquires data on the state transition specification 111A and the event constraint 111B, verifies whether or not an event has occurred in the state transition specification 111A that violates the rules stipulated by the event constraint 111B, and outputs the result as specification verification result data 120.

The specification comparison unit 40 pre-stores a comparison state transition specification for comparison with the state transition specification 111A, and compares the state transition specification 111A with the comparison state transition specification to extract differences.

The specification comparison unit 40 compares state transition specifications between multiple specifications. In FIG. 1, it compares the state transition specification 111A included in the system 1 formulated specification data 111 with the state transition specification (corresponding to the comparison state transition specification) included in the system 2 formulated specification data 112. Here, the system 1 formulated specification data 111 and the system 2 formulated specification data 112 registered by the specification registration unit 20 are both formulated according to predetermined standards. This makes it possible to perform the above-mentioned comparison mechanically. The specification comparison unit 40 outputs the comparison results, i.e., data related to the differences extracted by comparing the state transition specification with the comparison state transition specification, as specification comparison result data 130.

In addition to the above-mentioned components, the specification verification support device 1 may also include at least one of an input device, an output device, and a communication device. The processor, memory, input device, output device, and communication device included in the specification verification support device 1 are communicatively connected to each other via communication means such as a bus.

An input device is a device that accepts input from a user. Examples of input devices include a keyboard, mouse, touch panel, card reader, and voice input device.

An output device is a device that provides various information such as processing progress and results to the user. Examples of output devices include screen display devices (Liquid Crystal Display (LCD), Head Mounted Display (HMD), etc.), audio output devices, and printing devices.

A communication device is a wired or wireless communication interface that enables communication with other devices via communication means such as a Local Area Network (LAN) or the Internet, and is, for example, a Network Interface Card (NIC), a wireless communication module, a Universal Serial Interface (USB) module, or a serial communication module.

The specification verification support device 1 may also be configured to input and output information to and from other devices via a communication device.

Figure 2 is a conceptual diagram showing the internal structure of the formulated specification data corresponding to at least one embodiment of the present disclosure.

The formalized specification data in Figure 2 corresponds, for example, to the System 1 formalized specification data 111 in Figure 1. Formalized specification data expresses the specifications of an information system based on at least multiple models and inter-model events.

A model corresponds to a single process, such as "order entry" in an e-commerce system. Models contain state transition specification data and event constraint data. Models are connected by inter-model events.

State transition specification data is data that specifies state transitions due to events for each of multiple models. An event refers to any event or action that occurs in an information system. For example, receiving a message indicating that a product has been shipped, or sending a message indicating that a product has been shipped to another processing unit, device, or system, would be considered an event here. Events include events that occur in other models due to the state transitions of a model.

Event constraint data is data that specifies the violations that must be violated when an event occurs.

As conceptually shown in Figure 2, when the specifications of an information system are formulated according to predetermined standards that connect multiple models with inter-model events, it becomes easier to discover overlooked or missing aspects in the specifications. Furthermore, because the specification data formulated as described above is structured according to uniform standards, it becomes easier to compare specifications between multiple information systems. A more specific example of the format of such formulated specification data will be described later with reference to Figure 4.

Figure 3 is a flowchart illustrating a system specification determination process corresponding to at least one embodiment of the present disclosure. Below, each process described with the specification verification support device 1, specification registration unit 20, specification verification unit 30, or specification comparison unit 40 as the processing entity may be performed mechanically by each processing entity, or may request user input from a user such as a person in charge as needed and perform the processing using the information entered by the user.

A person in charge (human) describes the system specifications of the information system in free format (S11). The free format may be, for example, UML format or natural language format.

The specification registration unit 20 registers the system specifications (S12). The system specifications are registered in a formalized format. Detailed processing of step S12 will be described later.

The specification verification unit 30 performs system specification verification (S13). Detailed processing of step S13 will be described later.

The specification comparison unit 40 performs system specification comparison and verification (S14). Detailed processing of step S14 will be described later.

Figure 4 is a conceptual diagram illustrating the format of the formalized specification data corresponding to at least one embodiment of the present disclosure.

The formalized specification data includes event information, model information, state transition information, and event constraint information. Note that the state transition information corresponds to state transition specification 111A in Figure 1, and the event constraint information corresponds to event constraint 111B in Figure 1.

Event information includes the following items: event name, business procedure name, model name, standard/exception classification, and main/sub classification.

Model information includes the model name as an item.

State transition information includes the following items: event name, business procedure name, model name, state name, event result, and destination state name.

Event constraint information includes the following report items: event name, business procedure name, constraint type, and constraint content.

Figure 5 is a flowchart illustrating system specification registration corresponding to at least one embodiment of the present disclosure. Figure 6 is a flowchart illustrating system specification registration corresponding to at least one embodiment of the present disclosure. The system specification registration process shown in Figures 5 and 6 corresponds to step S12 in Figure 3.

First, the specification registration unit 20 extracts events from the free-form specification description (S21).

The specification registration unit 20 determines whether a model that is the target of the event already exists (S22). If a model already exists, the process proceeds to step S23; if not, the process proceeds to step S24.

In step S23, the specification registration unit 20 determines an already existing model as the model that will be the target of the event.

In step S24, the specification registration unit 20 newly registers the model that is the target of the event.

In step S25, the specification registration unit 20 determines the business procedure name. In step S26, the specification registration unit 20 determines the event name.

The specification registration unit 20 determines whether the event in question is a process that is required under normal circumstances (S27). If the event in question is a process that is always performed under normal circumstances, processing transitions to step S28, where the specification registration unit 20 determines the standard/exception classification of the event to be "standard." If the event in question is a process that is performed when an error occurs, or a process that is performed under normal circumstances but is not necessarily performed, processing transitions to step S29, where the specification registration unit 20 determines the standard/exception classification of the event to be "exception."

After step S28 or S29, processing transitions to step S31 shown in Figure 6.

In step S31, the specification registration unit 20 determines whether the event in question is an event that changes the state of a portion of an attribute of the target model. If the event in question is an event that changes the state of a model, processing transitions to step S32, where the specification registration unit 20 determines the main/sub-category of the event to be a "main event." If the event in question is an event that changes the state of a portion of an attribute of the model, processing transitions to step S33, where the specification registration unit 20 determines the main/sub-category of the event to be a "sub-event."

Note that it is not necessary to categorize events as primary/secondary. If multiple events were to be interpreted as different types of events, even when they merely change the state of some attributes of a model, the number of event types would increase dramatically, resulting in a large processing load. To avoid this, events that merely change the state of some attributes of a model are managed as secondary events derived from primary events. This helps to prevent an increase in processing load.

In step S34, the specification registration unit 20 determines whether there are any unprocessed events in the free-form specification description. If there are any unprocessed events, processing transitions to step S21 in Figure 5, where the specification registration unit 20 retrieves and processes the next unprocessed event. If there are no unprocessed events remaining, processing transitions to step S35.

The specification registration unit 20 performs event registration (standard) processing (S35). The specification registration unit 20 performs event registration (exception) processing (S36). The specification registration unit 20 performs event registration (sub-event) processing (S37).

The specification registration unit 20 performs event registration (procedure result) processing (S38). The specification registration unit 20 performs constraint condition registration processing (S39).

Details of steps S35 to S39 will be described later.

Figure 7 is a flowchart illustrating an example of event registration (standard) processing corresponding to at least one embodiment of the present disclosure. Note that the event registration (standard) processing corresponds to step S35 in Figure 6.

The specification registration unit 20 registers the event (standard) in the target model (S41).

The specification registration unit 20 determines whether there are any unregistered events (S42). If there are any unregistered events, the process returns to step S41, where the specification registration unit 20 registers the next event. If there are no unregistered events, the process proceeds to step S43.

In step S43, the specification registration unit 20 determines the state transition of the model due to the event. That is, it determines how the state of the target model will transition due to the event. This determination process may be performed by the specification registration unit 20 outputting information to an output device such as a monitor that prompts the person in charge to input or select the state transition of the model due to the event, and accepting user input, for example. For example, the person in charge specifies the order between events using an input device. The specification registration unit 20 determines the state transition according to the specified order.

The specification registration unit 20 determines whether there are any events whose state transitions have not been registered (S44). If there are any events whose state transitions have not been registered, the process returns to step S43. If there are no events whose state transitions have not been registered, the process shown in Figure 7 ends.

Figure 8 is a diagram illustrating an example of event registration (standard) processing corresponding to at least one embodiment of the present disclosure. This example illustrates the case where standard events numbered 1 to 5 are added to a model (order).

The model (order) has six states: initial state S0, order received state S1, inventory confirmed state S2, prepared for shipping state S3, shipped state S4, and completed state S5. The states transition depending on the occurrence of some event.

Five events were registered in the model (order) according to the flow shown in Figure 7. For example, the following event was registered as number 1:
Event: Order occurrence Business procedure: Order entry Model: Order Standard/Exception classification: Standard

Similarly, Figure 8 shows the results of registering events numbered 2 through 5. The "Procedure Result" column in the registered data is blank at this point. The state transition (see step S43 in Figure 8) column is set to the setting value shown in Figure 8. For example, if the event "Order Placed" occurs in state S0, the state will transition from S0 to S1. "E" in the state transition column indicates an error. For example, it would be strange for a shipping preparation event to occur in state S4 (shipped). In such a case, the information system needs to perform some kind of error processing, so the setting value in the state transition column is set to "E." The setting value "-" in the state transition column indicates that the state transition in question cannot occur in the first place.

Figure 9 is a flowchart illustrating an example of event registration (exception) processing corresponding to at least one embodiment of the present disclosure. Note that the event registration (exception) processing corresponds to step S36 in Figure 6.

The specification registration unit 20 registers an event (exception) in the target model (S51).

The specification registration unit 20 determines whether there are any unregistered events (S52). If there are any unregistered events, the process returns to step S51, where the specification registration unit 20 registers the next event. If there are no unregistered events, the process proceeds to step S53.

In step S53, the specification registration unit 20 determines the state transition of the model due to the event (exception). That is, it determines how the state of the target model will transition due to the exceptional event. This determination process may be performed by the specification registration unit 20 outputting information to an output device such as a monitor that prompts the person in charge to input or select the state transition of the model due to the event, and accepting user input, for example. For example, the person in charge specifies the order between events using an input device. The specification registration unit 20 determines the state transition according to the specified order.

The specification registration unit 20 determines whether there are any events whose state transitions have not been registered (S54). If there are any events whose state transitions have not been registered, processing returns to step S53. If there are no events whose state transitions have not been registered, processing proceeds to step S55.

In step S55, the specification registration unit 20 determines whether there is a state to be added to the model due to the event (exception). If there is a state to be added, the process proceeds to step S56. If there is no state to be added, the process shown in Figure 9 ends.

In step S56, the specification registration unit 20 adds states to the model and determines state transitions due to events (standard).

Figure 10 is a diagram illustrating an example of event registration (exception) processing corresponding to at least one embodiment of the present disclosure. This example illustrates the case where an exception event number 6 is added to a model (order).

As mentioned above, the model (order) has six states: initial state S0, order received state S1, inventory confirmed state S2, prepared for shipping state S3, shipped state S4, and completed state S5. The states transition depending on the occurrence of an event. Five standard events have already been registered for the model (order) according to the flow shown in Figure 7.

A new exception event has been registered in the model (order) according to the flow shown in Figure 9. For example, the following event has been registered as number 6.

Event: Cancelled Business Procedure: -
Model: Order Standard/Exception Classification: Exception

The result of registering exception event number 6 is shown in Figure 10. The "Procedure Result" column in the registered data is blank at this point. The meanings of the setting values "E" and "-" in the state transition column are the same as those described above with reference to Figure 8, so a detailed explanation will be omitted.

If an exception event requires an addition to the model's state transitions, the addition is made (see step S56 in Figure 9). Although not shown in the figure, for example, state S6 is newly added. At this time, the specification registration unit 20 also determines the state transition for state S6. In other words, a setting value is also set in the state S6 column.

Figure 11 is a flowchart illustrating an example of event registration (sub-event) processing corresponding to at least one embodiment of the present disclosure. Note that the event registration (sub-event) processing corresponds to step S37 in Figure 6.

The specification registration unit 20 registers the sub-event in the target model and the sub-model (S61). Note that the sub-model will be described later with reference to Figure 12.

The specification registration unit 20 determines whether there are any unregistered sub-events (S62). If there are any unregistered sub-events, the process returns to step S61, where the specification registration unit 20 registers the next sub-event. If there are no unregistered sub-events, the process proceeds to step S63.

In step S63, the specification registration unit 20 determines the state transition of the target model due to the sub-event. That is, it determines how the state of the target model will transition due to the sub-event. This determination process may be performed by the specification verification support device 1 outputting information to an output device such as a monitor that prompts the person in charge to input or select the state transition of the model due to the sub-event, and accepting user input, for example. For example, the person in charge specifies the order between events using an input device. The specification registration unit 20 determines the state transition according to the specified order.

The specification registration unit 20 determines whether the target model contains any sub-events whose transition destinations (state transitions) are unregistered (S64). If there are any sub-events whose transition destinations (state transitions) are unregistered, processing returns to step S63. If there are no sub-events whose transition destinations (state transitions) are unregistered, processing proceeds to step S65.

In step S65, the specification registration unit 20 determines the state transition of the secondary model due to the secondary event. That is, it determines how the state of the target secondary model will transition due to the secondary event. This determination process may be performed by the specification registration unit 20 outputting information to an output device such as a monitor that prompts the person in charge to input or select the state transition of the secondary model due to the secondary event, and accepting user input, for example. For example, the person in charge specifies the order between events using an input device. The specification registration unit 20 determines the state transition according to the specified order.

The specification registration unit 20 determines whether there is a sub-event in the sub-model whose transition destination (state transition) is not registered (S66). If there is a sub-event whose transition destination (state transition) is not registered, the process returns to step S65. If there is no sub-event whose transition destination (state transition) is not registered, the process shown in Figure 11 ends.

Figure 12 is a diagram showing an example of event registration (sub-event) processing corresponding to at least one embodiment of the present disclosure.

As a result of performing the event registration (sub-event) process shown in Figure 11 from the registration state shown in Figure 10, the event "Deposit" and event "Refund" were added to the target model. Number 7 is the event "Deposit". Number 8 is the event "Refund". In addition, events similar to numbers 1 to 8 added to the target model were added to the sub-model.

Now, we will explain sub-models. A sub-model is a model derived from a target model (main model). The specification registration unit 20 registers and manages state transitions for each model. As the number of target models increases, the structure of the formalized specification data (see Figure 2) becomes more complex, and the processing load for various processes based on the formalized specification data also increases. Therefore, models that only differ in some attributes from the target model are not treated as main models, but as derived models (sub-models) subordinate to the main model. The state transition specification then defines transitions by treating secondary states derived from specific states of a model (main model) as states of the model's sub-models. This prevents an explosive increase in the number of model types and reduces the processing load.

In the example shown in Figure 12, the main model (order) has six states: initial state S0, order received state S1, inventory confirmed state S2, prepared for shipping state S3, shipped state S4, and completed state S5, and these states transition depending on the occurrence of an event. Meanwhile, the sub-model (payment state) derived from the main model (order) has five states: initial state SS0, waiting for payment state SS1, paid state SS2, waiting for refund state SS3, and refunded state SS4, and these states transition depending on the occurrence of an event.

Sub-events were registered in the model (order) and the sub-model (deposit processing) derived from the model (order) according to the flow shown in Figure 11. For example, the following sub-event "deposit" is registered:

Event: Deposit Business procedure: -
Model: Order Standard/Exception Classification: Standard Primary/Secondary Classification: Secondary

The secondary event "Refund" will also be registered in the same way.

Figure 12 shows the results of registering these secondary events. The meanings of the setting values "E" and "-" in the State Transition column are the same as those described above with reference to Figure 8, so a detailed explanation will be omitted. The setting value "(SS)" in the State Transition column means that a state transition does not occur in the main model, but rather the event that occurs is managed by the secondary model.

Figure 13 is a flowchart illustrating an example of event registration (procedure result) processing corresponding to at least one embodiment of the present disclosure. Note that the event registration (procedure result) processing corresponds to step S38 in Figure 6.

At the end of step S37 in Figure 6, the procedure result fields in the models (main model and sub-model) were blank. The event registration (procedure result) process sets a setting value in the procedure result field.

The specification registration unit 20 records (sets) the procedure results for the target model (S71).

The specification registration unit 20 determines whether there are any lines in the target model where the procedure result has not been recorded (S72). If there are any lines where the procedure result has not been recorded, the process returns to step S71, where the specification registration unit 20 records the next procedure result. If there are no lines where the procedure result has not been recorded, the process proceeds to step S73.

The specification registration unit 20 divides the event and determines the procedure result and state transition (S73).

The specification registration unit 20 determines whether the target model contains any lines in which procedure results and state transitions are not yet described (S74). If there are any lines in which they are not yet described, the process returns to step S73. If there are no lines in which they are not yet described, the process proceeds to step S75.

The specification registration unit 20 determines whether there are any states to add to the target model (S75). If there are any states to add, the process proceeds to step S76. If there are no states to add, the process shown in Figure 13 ends.

In step S76, the specification registration unit 20 adds a state to the target model and determines the state transitions for the added state due to existing (registered) events (S76).

Figure 14 is a diagram showing an example of event registration (procedure result) processing corresponding to at least one embodiment of the present disclosure.

In step S71, an entry is made in the procedure result column for the "Order" model. Entering means setting a setting value. Here, when the "Prepare for Shipping" event occurs, the business procedure on the information system side is an inventory check. Since inventory is not always available in reality, the procedure results of the business procedure are divided into two cases: when there is inventory and when there is no inventory. Furthermore, for the arrival of goods, since all packages may arrive in reality or only some of the packages may arrive (with the remaining packages arriving at different times), the procedure results are divided into two cases: when some packages arrive and when all packages arrive. In this way, when considering the specific business procedure at the time an event occurs, if the procedure's outcome can branch into two or more outcomes, the event is divided. As an example shown in Figure 14, the processing in step S73 divided event number 2, "Prepare for Shipping," into four events: number 2, number 2-1, number 2-2, and number 2-3. The procedure results and state transitions are then determined and set as setting values.

In step S75, it was determined that a state for backordering should be added to the "Order" model, so in step S76, state S11 (backordering) is added. The state transitions due to existing events for the added state S11 (backordering) are set as the setting values. The existing events here refer to events numbered 1 to 8, and also include the events numbered 2-1, 2-2, and 2-3 after the division.

In other words, when there are multiple procedure results in a business procedure corresponding to an event to a model, the specification registration unit 20 splits the event to the model into multiple events corresponding to the procedure results in the state transition specification, and accepts registration in the state transition specification of the states that are added as a result of the event being split into multiple events and the state transitions related to the added states.

Figure 15 is a flowchart illustrating a constraint registration process corresponding to at least one embodiment of the present disclosure. Note that the constraint registration process corresponds to step S39 in Figure 6.

The specification registration unit 20 registers event constraints (occurrence order) (S81). More specifically, it registers in the system specification 110 what prerequisite events must have occurred before a certain event occurs. For example, an order occurrence event must have occurred before a deposit event. Therefore, the above event constraints are registered so that cases in which a deposit event occurs even though an order occurrence event has not occurred can be extracted as a contradiction in the specification.

The above event constraint, which specifies the order in which multiple events occur, is referred to as the first constraint. In step S92, which will be described later, the specification verification unit 30 checks whether events in the state transition specification can occur in an order different from the order specified in the first constraint.

The specification registration unit 20 registers the event constraint (occurrence time) (S82). More specifically, the specific time when the event will occur is registered in the system specification 110. This makes it possible to extract an event that occurs at a time different from the registered time as a contradiction in the specification.

The above event constraint that specifies when an event occurs is referred to as the second constraint. In step S92, which will be described later, the specification verification unit 30 checks whether an event can occur at a time in the state transition specification that differs from the time specified in the second constraint.

The specification registration unit 20 registers the event constraints (model CRUD) (S83). CRUD is a coined word combining the initial letters of Create, Refer, Update, and Delete (D). In other words, the specification registration unit 20 registers in the system specification 110 what information, objects, etc. are created, referred to, updated, or deleted in the information system's processing in response to an event for the target model. This allows for the extraction of specification inconsistencies that are clearly irrational from the CRUD perspective when multiple events are arranged in chronological order. For example, an event sequence in which information is referred to (R), updated (U), or deleted (D) before that information has yet to be created (C) is clearly irrational. Similarly, an event sequence in which information is referred to (R) or updated (U) after it has been deleted (D) is clearly irrational. When checking whether or not such an obviously irrational sequence of events exists, registered CRUD information is used.

In other words, the model includes a model that generates, references, updates, or deletes information in response to the occurrence of an event. The above event constraint, which specifies the order in which information is created, read, updated, or deleted by the model, is referred to as the third constraint. In step S92, which will be described later, the specification verification unit 30 checks whether information is created, read, updated, or deleted in an order different from the order specified in the third constraint in the state transition specification.

The specification registration unit 20 registers the event constraint (secondary model CRUD) (S84). The content of the registered information is the same as in step S83. In step S84, for the secondary model, the system specification 110 registers what data is created, referenced, updated, or deleted in the processing of the information system in response to the occurrence of an event.

In other words, the secondary model includes a model that generates, references, updates, or deletes information in response to the occurrence of an event. The event constraint that specifies the order in which information is created, read, updated, or deleted by the secondary model is referred to as the fourth constraint. In step S92, which will be described later, the specification verification unit 30 checks whether information is created, read, updated, or deleted in an order different from the order specified in the fourth constraint in the state transition specification.

Figure 16 is a flowchart illustrating a system verification process corresponding to at least one embodiment of the present disclosure. The system verification process corresponds to step S13 in Figure 3.

The specification verification unit 30 checks for unspecified items (S91). For example, if there is a point in the corresponding target model or sub-model where the state transition destination has not been set for each event, the specification verification unit 30 extracts that point as a contradiction.

The specification verification unit 30 checks for constraint violations (S92). More specifically, the specification verification unit 30 checks all combinations of events and state transitions based on the formalized specification data registered in the system specification 110. If, during this check of all combinations, an inconsistency based on the various event constraints registered by the specification registration unit 20 (see Figure 15) is discovered, the inconsistency is extracted as a contradiction.

The specification verification unit 30 outputs the inconsistencies (S93). That is, the inconsistencies extracted in step S91 or step S92 are output via an output device. For example, if the output device is a monitor, a list of the extracted inconsistencies is displayed on the monitor as the check results.

The person in charge corrects the inconsistencies based on the output information indicating the inconsistencies. Based on the corrections input by the person in charge, the specification registration unit 20 registers various information in the system specifications 110 in the same manner as described above with reference to Figures 5 to 15 (S94).

Figure 17 is a conceptual diagram illustrating the format of specification verification result data corresponding to at least one embodiment of the present disclosure.

The specification verification result data 120 includes specification inconsistency information. This specification inconsistency information is used in the inconsistency output process in step S93. Figure 16 shows the format of the specification inconsistency information that expresses inconsistencies regarding state transitions.

The specification inconsistency information in the format shown in Figure 17 has the following items: Model 1, State Name 1, Model 2, State Name 2, Occurring Event Name, and Reason for Transition Failure. In other words, if a transition from a certain state in Model 1 (State Name 1) to a certain state in Model 2 (State Name 2) fails, the name of the occurring event that caused the transition and the reason the state transition was not possible are recorded as specification inconsistency information in the specification verification result data 120. Note that for inconsistencies related to state transitions within the same model, the Model 1 or Model 2 item can be left blank, or the same model as set in Model 1 can be set in Model 2.

Note that the format of the specification contradiction information is not limited to that shown in Figure 17, and a person skilled in the art may set a format appropriate to the content of the contradiction.

Figure 18 is a flowchart illustrating a system specification comparison and verification process corresponding to at least one embodiment of the present disclosure. The system specification comparison and verification process corresponds to step S14 in Figure 3.

The specification comparison unit 40 performs a system specification comparison process (S101). Details of the system specification comparison process will be described later. The results of the system specification comparison process are stored as specification comparison result data 130, and the data management unit 10 manages the specification comparison result data 130.

The specification comparison unit 40 outputs the differences in the system specifications (S102). That is, the differences in the system specifications extracted in step S101 are output via an output device. For example, if the output device is a monitor, a list of the extracted differences is displayed on the monitor as the check results.

The person in charge modifies the system specifications based on the output information indicating the differences. Based on the modifications input by the person in charge, the specification registration unit 20 registers various information in the system specifications 110 in the same manner as described above with reference to Figures 5 to 15 (S103).

Next, the system specification comparison process will be described in detail. System specification comparison is performed between the specifications of multiple systems based on the formalized specification data shown in Figure 2. For example, the system 1 formalized specification data 111 and the system 2 formalized specification data 112 shown in Figure 1 are compared. Note that the specifications of three or more types of systems may be compared simultaneously. The following explanation will be given using an example where the specifications of two types of systems are compared.

The specification comparison unit 40 compares the model configurations (S111). More specifically, it compares the lists of models present in the system between the specifications of multiple systems. This comparison corresponds to a model configuration comparison in which the list of models present in the state transition specification is compared with the list of models present in the comparison state transition specification to extract any deficiencies or excesses in models.

The specification comparison unit 40 compares the event configurations (S112). More specifically, it compares the event lists for each model between the specifications of multiple systems. This comparison corresponds to an event configuration comparison in which, for each model in the state transition specification, the event list is compared with the model in the comparison state transition specification corresponding to the model to extract any excess or deficiency of events.

The specification comparison unit 40 compares the state configurations (S113). More specifically, it compares the state lists for each model between the specifications of multiple systems. This comparison corresponds to a state configuration comparison in which, for each model in the state transition specification, the state list is compared with the model in the comparison state transition specification that corresponds to that model to extract any excess or deficiency of states.

The specification comparison unit 40 compares the transition destination configurations (S114). More specifically, it compares the transition destinations when the same event occurs for each model between the specifications of multiple systems. This comparison corresponds to a transition destination comparison in which, for each model in the state transition specification, the transition destination states for the corresponding events are compared with the model in the comparison state transition specification to extract the differences in the transition destinations.

The specification comparison unit 40 compares the constraints (S115). More specifically, it compares the lists of registered event constraints (violations) between the specifications of multiple systems.

Here, the system specifications, including data related to event constraints, are stored in advance in the system specifications 110 as the above-mentioned formalized specification data in a format that conforms to predetermined standards. Therefore, the specification comparison unit 40 can mechanically perform the above-mentioned comparison between the specifications of multiple systems.

The above-mentioned constraint comparison corresponds to a constraint comparison in which comparison event constraints, which are event constraints corresponding to the comparison state transition specifications, are stored in advance, and the specification comparison unit 40 compares a list of violations between the event constraints corresponding to the state transition specifications and the comparison event constraints to extract any excesses or deficiencies in the violations.

Figure 19 is a conceptual diagram illustrating the format of specification comparison result data corresponding to at least one embodiment of the present disclosure.

The specification comparison result data 130 includes specification inconsistency information, difference information (model configuration comparison), difference information (event configuration comparison), difference information (state configuration comparison), difference information (transition destination comparison), and difference information (constraint comparison). Note that the classification and format of each piece of information shown in Figure 19 are merely examples, and those skilled in the art may set the classification and format appropriately according to the content of the specification comparison results they wish to obtain.

The specification inconsistency information includes the following items: system name 1, system name 2, and difference information. The difference information in the specification inconsistency information corresponds to at least one of difference information (model configuration comparison), difference information (event configuration comparison), difference information (state configuration comparison), difference information (transition destination comparison), and difference information (constraint comparison).

Difference information (model configuration comparison) includes the model name and the name of the system that does not have it as items. For example, if system A has the model "Deposit," but system B does not have the model "Deposit," the difference information (model configuration comparison) will be (Deposit, System B). Note that the "Name of the system that does not have it" item is handled in the same way for other difference information described below, so detailed explanation will be omitted to avoid duplication.

Difference information (event configuration comparison) includes the event name, business procedure name, model name, and the name of the system that does not have the event.

Difference information (state configuration comparison) includes the model name, state name, and the name of the missing system.

The difference information (transition destination comparison) includes the following items: event name, business procedure name, model name, state name, transition destination of System 1, and transition destination of System 2. "Transition destination" here refers to the state (state name) of the transition destination.

Difference information (constraint comparison) includes the following items: event name, business procedure name, constraint type, constraint content, and the name of the system that does not have the constraint. Constraint type refers to types such as "occurrence order," "occurrence time," "model CRUD," and "sub-model CRUD" in Figure 15.

The above-described embodiments of the present invention are illustrative examples of the present invention and are not intended to limit the scope of the present invention to these embodiments alone. Those skilled in the art may implement the present invention in various other forms without departing from the scope of the present invention.

As described above, the specification verification support device 1, which supports specification verification of an information system, has a specification registration unit 20 that accepts registration of a state transition specification 111A that specifies state transitions due to events in each of a plurality of models, where the events include events that occur in other models due to the state transition of the model, and an event constraint 111B that specifies violations that should be considered when the event occurs. The specification verification support device 1 has a specification verification unit 30 that verifies whether any events that correspond to violations in the state transition specification 111A have occurred. This allows the state transition specification, including events that occur in other models due to the state transition of the model, to be registered, and the state transition specification is checked for occurrence of any events that correspond to violations during system specification verification, thereby reducing the chance of overlooking errors in the system specification.

The specification verification support device 1 pre-stores a comparison state transition specification for comparison with the state transition specification 111A, and further includes a specification comparison unit 40 that compares the state transition specification 111A with the comparison state transition specification to extract differences. This makes it possible to present differences by comparing with, for example, the state transition specification of a proven information system of the same type, and assist in the discovery of errors in the system specifications.

The specification comparison unit 40 performs at least one of the following: a model configuration comparison that compares a list of models in the state transition specification 111A with a list of models in the comparison state transition specification to extract whether there are any excess or deficiencies in the models; an event configuration comparison that compares a list of events for each model in the state transition specification 111A with a model in the comparison state transition specification corresponding to that model to extract whether there are any excess or deficiencies in the events; a state configuration comparison that compares a list of states for each model in the state transition specification 111A with a model in the comparison state transition specification corresponding to that model to extract whether there are any excess or deficiencies in the states; and a transition destination comparison that compares, for each model in the state transition specification 111A, with a model in the comparison state transition specification corresponding to that model to extract differences in the transition destinations for corresponding events. This makes it possible to compare models in the state transition specification and the comparison state transition specification and present the differences, thereby assisting in the discovery of errors in each model in the system specifications.

Comparison event constraints, which are event constraints corresponding to the comparison state transition specifications, are further stored in advance. The specification comparison unit 40 further performs constraint comparison, comparing a list of violations between the event constraints corresponding to the state transition specifications 111A and the comparison event constraints, to extract any excesses or deficiencies in the violations. This presents event violations between the state transition specifications and the comparison state transition specifications, making it possible to assist in the discovery of errors related to the event constraints in the system specifications.

The event constraints include a first constraint that specifies the order in which multiple events occur. The specification verification unit 30 checks whether events in the state transition specification 111A can occur in an order different from the order specified in the first constraint. This makes it easy to discover errors in the system specifications regarding the order in which events occur.

The event constraint includes a second constraint that specifies when the event will occur. The specification verification unit 30 checks whether the event can occur at a time different from the time specified in the second constraint in the state transition specification 111A. This makes it easy to discover errors in the system specifications regarding the timing of event occurrence.

The models include models that generate, reference, update, or delete information in response to the occurrence of an event. The event constraints include a third constraint that specifies the order in which information is created, read, updated, and deleted by the model. The specification verification unit 30 checks whether information is created, read, updated, or deleted in an order different from the order specified in the third constraint in the state transition specification. This makes it possible to verify the consistency of the order of events across models, such as when information created in one model is read by another model.

State transition specification 111A defines transitions by treating secondary states derived from specific states of a model as states of sub-models of the model. This prevents an explosive increase in the number of combinations of model states and events in state transition specifications that include events between models.

The secondary model includes a model that generates, references, updates, or deletes information in response to the occurrence of an event. The event constraint includes a fourth constraint that specifies the order in which information is created, read, updated, or deleted by the secondary model. The specification verification unit 30 checks whether information is created, read, updated, or deleted in an order different from the order specified in the fourth constraint in the state transition specification. This makes it possible to verify the consistency of the order of events, including the secondary model.

When there are multiple procedure results in a business procedure corresponding to an event to a model, the specification registration unit 20 splits the event to the model into multiple events corresponding to the procedure results in the state transition specification 111A, and accepts registration in the state transition specification 111A of the states that are added as a result of the event being split into multiple events and the state transitions related to the added states. This makes it possible to support the registration of state transition specifications that can be used to verify system specifications that include events that occur in other models due to state transitions in a model.

In a specification verification support method for supporting specification verification of an information system, a device 1 equipped with a processor and memory accepts registration of a state transition specification 111A that specifies state transitions due to events for each of a plurality of models, where the events include events that occur in other models due to the state transition of the model, and an event constraint 111B that specifies violations that should be considered when the event occurs, and verifies whether any events that fall under the violations in the state transition specification 111A have occurred. This registers a state transition specification that includes events that occur in other models due to the state transition of a model, and checks whether any events that fall under the violations in the state transition specification have occurred during system specification verification, thereby reducing the chance of overlooking errors in the system specification.

A specification verification support program that supports specification verification of an information system causes a device (1) equipped with a processor and memory to accept registration of state transition specifications (111A) that specify state transitions due to events in each of a plurality of models, where the events include events that occur in other models due to the state transition of the model, and event constraints (111B) that specify violations that should be considered when the event occurs, and to verify whether any events that correspond to violations in the state transition specifications have occurred. This registers state transition specifications that include events that occur in other models due to the state transition of a model, and checks for the occurrence of events that correspond to violations in the state transition specifications during system specification verification, thereby reducing the chance of overlooking errors in the system specifications.

1... specification verification support device, 10... data management section, 20... specification registration section, 30... specification verification section, 40... specification comparison section

Claims (11)

A specification verification support device that supports specification verification of an information system,
a specification registration unit that accepts registration of state transition specifications that define state transitions due to events in each of a plurality of models, the events including events that occur in other models due to state transitions of the models, and event constraints that define violations that should be considered when the events occur;
a specification verification unit that verifies whether or not an event corresponding to the violation in the state transition specification occurs;
a specification comparison unit that stores in advance a comparison state transition specification for comparison with the state transition specification, and compares the state transition specification with the comparison state transition specification to extract differences ;
A specification verification support device having the above configuration. The specification comparison unit
a model configuration comparison that compares a list of models in the state transition specification with a list of models in the comparison state transition specification to extract excesses and deficiencies of models;
an event configuration comparison for comparing a list of events for each model in the state transition specification with a model in the comparison state transition specification corresponding to the model, and extracting excess or deficiency of events;
a state configuration comparison for comparing a list of states for each model in the state transition specification with a model in the comparison state transition specification corresponding to the model, and extracting excess or deficiency of states;
a transition destination comparison for comparing, for each model in the state transition specification, a model in the comparison state transition specification corresponding to the model, with a transition destination state for a corresponding event, and extracting a difference in the transition destination;
Execute at least one of
2. The specification verification support device according to claim 1 . a comparison event constraint corresponding to the comparison state transition specification is further stored in advance;
the specification comparison unit further performs a constraint comparison to compare a list of violations between the event constraint corresponding to the state transition specification and the comparison event constraint, and extracts excesses and deficiencies of violations.
The specification verification support device according to claim 1 . A specification verification support device that supports specification verification of an information system,
a specification registration unit that accepts registration of state transition specifications that define state transitions due to events in each of a plurality of models, the events including events that occur in other models due to state transitions of the models, and event constraints that define violations that should be considered when the events occur;
a specification verification unit that verifies whether or not an event corresponding to the violation in the state transition specification occurs;
and
The model includes a model that generates, references, updates, or deletes information in response to an occurrence of an event;
the event constraints include a third constraint that specifies the order in which information is created, read, updated, and deleted by the model;
the specification verification unit checks whether or not information is created, read, updated, or deleted in an order different from the order defined in the third constraint in the state transition specification .
Specification verification support device. A specification verification support device that supports specification verification of an information system,
a specification registration unit that accepts registration of state transition specifications that define state transitions due to events in each of a plurality of models, the events including events that occur in other models due to state transitions of the models, and event constraints that define violations that should be considered when the events occur;
a specification verification unit that verifies whether or not an event corresponding to the violation in the state transition specification occurs;
and
When a business procedure corresponding to an event to a model has a plurality of procedure results, the specification registration unit divides the event to the model into a plurality of events corresponding to the procedure results in the state transition specification, and accepts registration of states that are added as a result of the event being divided into a plurality of events and state transitions related to the added states in the state transition specification .
Specification verification support device. A specification verification support method for supporting specification verification of an information system, comprising:
1. An apparatus comprising a processor and a memory,
A system that accepts registration of a state transition specification that specifies a state transition due to an event for each of a plurality of models, the state transition specification including an event that occurs in another model due to the state transition of the model, and an event constraint that specifies a violation that should be considered when the event occurs,
Verifying whether or not an event corresponding to the violation in the state transition specification has occurred;
storing in advance a comparison state transition specification for comparison with the state transition specification, and comparing the state transition specification with the comparison state transition specification to extract differences ;
A specification verification support method that performs the above. A specification verification support method for supporting specification verification of an information system, comprising:
1. An apparatus comprising a processor and a memory,
A system that accepts registration of a state transition specification that specifies a state transition due to an event for each of a plurality of models, the state transition specification including an event that occurs in another model due to the state transition of the model, and an event constraint that specifies a violation that should be considered when the event occurs,
verifying whether or not an event corresponding to the violation in the state transition specification has occurred;
It is a way of doing things,
The model includes a model that generates, references, updates, or deletes information in response to an occurrence of an event;
the event constraints include a third constraint that specifies the order in which information is created, read, updated, and deleted by the model;
confirming whether or not the state transition specification allows information to be created, read, updated, or deleted in an order different from the order specified in the third constraint;
Specification verification support method. A specification verification support method for supporting specification verification of an information system, comprising:
1. An apparatus comprising a processor and a memory,
A system that accepts registration of a state transition specification that specifies a state transition due to an event for each of a plurality of models, the state transition specification including an event that occurs in another model due to the state transition of the model, and an event constraint that specifies a violation that should be considered when the event occurs,
verifying whether or not an event corresponding to the violation in the state transition specification has occurred;
It is a way of doing things,
When a business procedure corresponding to an event to a model has multiple procedure results, the state transition specification divides the event to the model into multiple events corresponding to the procedure results, and accepts registration of states that are added as a result of the event being divided into multiple events and state transitions related to the added states in the state transition specification.
Specification verification support method. A specification verification support program for supporting specification verification of an information system,
An apparatus comprising a processor and a memory,
A system that accepts registration of a state transition specification that specifies a state transition due to an event for each of a plurality of models, the state transition specification including an event that occurs in another model due to the state transition of the model, and an event constraint that specifies a violation that should be considered when the event occurs,
Verifying whether or not an event corresponding to the violation in the state transition specification has occurred;
storing in advance a comparison state transition specification for comparison with the state transition specification, and comparing the state transition specification with the comparison state transition specification to extract differences ;
A specification verification support program that helps you do this. A specification verification support program for supporting specification verification of an information system,
An apparatus comprising a processor and a memory,
A system that accepts registration of a state transition specification that specifies a state transition due to an event for each of a plurality of models, the state transition specification including an event that occurs in another model due to the state transition of the model, and an event constraint that specifies a violation that should be considered when the event occurs,
verifying whether or not an event corresponding to the violation in the state transition specification has occurred;
It is a program to make it happen,
The model includes a model that generates, references, updates, or deletes information in response to an occurrence of an event;
the event constraints include a third constraint that specifies the order in which information is created, read, updated, and deleted by the model;
checking whether or not information is created, read, updated, or deleted in an order different from the order specified in the third constraint in the state transition specification;
Specification verification support program. A specification verification support program for supporting specification verification of an information system,
An apparatus comprising a processor and a memory,
A system that accepts registration of a state transition specification that specifies a state transition due to an event for each of a plurality of models, the state transition specification including an event that occurs in another model due to the state transition of the model, and an event constraint that specifies a violation that should be considered when the event occurs,
verifying whether or not an event corresponding to the violation in the state transition specification has occurred;
It is a program to make it happen,
When a business procedure corresponding to an event to a model has a plurality of procedure results, the event to the model is divided into a plurality of events corresponding to the procedure results in the state transition specification, and states that are added as a result of the event being divided into a plurality of events and state transitions related to the added states are registered in the state transition specification.
Specification verification support program.