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

Abstract

To reduce the oversight of errors in verifying system specifications.SOLUTION: A specification verification support device that supports specification verification of an information system includes: a specification registration unit that accepts registration of state transition specifications that specify state transitions due to events in each of a plurality of models, in which the events include events that occur in other models due to state transitions of the models and event constraints that specify violation items that should be regarded as violations in relation to the events when the events occur; and a specification verification unit that verifies whether any event that corresponds to the violation items occurs in the state transition specifications.SELECTED DRAWING: Figure 2

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. After the client and developer confirm the system specifications, the information system is designed and created in accordance with the system 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 of Patent document 1 allows a system verifier to specify simplification of state transition specifications from a viewpoint 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, allows the verifier to input a viewpoint for degenerating the state transition table and the part to be degenerated in the sequence diagram, determines the content of degeneration of the state transition table based on the input viewpoint for degenerating the state transition table and the part to be degenerated in the sequence diagram, and generates data for the state transition table after degeneration from data representing the original state transition table.

JP 2010-250422 A

According to the disclosure of Patent Document 1, it is possible to support system verification by simplifying the state transition table based on a viewpoint 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 a technique that allows for a reduction in overlooking errors in verifying system specifications.

A specification verification support device according to one aspect of 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 a plurality of 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 violated 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.

A specification verification support method according to one aspect included in the present disclosure is a specification verification support method that supports specification verification of an information system, in which an apparatus having a processor and memory accepts registration of state transition specifications that specify state transitions due to events for each of a plurality of 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 violated when the events occur, and verifies whether any events that correspond to the violations have occurred in the state transition specifications.

A specification verification support program according to one aspect of the present disclosure is a specification verification support program that supports specification verification of an information system, and causes a device having 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 state transitions of the models, and event constraints that specify violations that should be violated when the events occur, and to verify whether any events that correspond to the violations have occurred in the state transition specifications.

According to one aspect of the present disclosure, it is possible to reduce the oversight of 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 corresponding to at least one of the embodiments of the present disclosure. FIG. 2 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 formulated specification data according to at least one embodiment of the present disclosure. 1 is a flowchart illustrating a system specification registration process according to at least one embodiment of the present disclosure. 1 is a flowchart illustrating a system specification registration process according to at least one embodiment of the present disclosure. 11 is a flowchart illustrating an example of an event registration (standard) process according to at least one embodiment of the present disclosure. FIG. 11 is a diagram illustrating a process example of an event registration (standard) process according to at least one of the embodiments of the present disclosure. 11 is a flowchart illustrating an event registration (exception) process according to at least one embodiment of the present disclosure. FIG. 11 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. 11 is a flowchart illustrating an event registration (sub-event) process according to at least one embodiment of the present disclosure. FIG. 11 is a diagram illustrating a processing example of an event registration (sub-event) process corresponding to at least one of the embodiments of the present disclosure. 11 is a flowchart illustrating an example of an event registration (procedure result) process according to at least one embodiment of the present disclosure. FIG. 11 is a diagram illustrating a processing example of an event registration (procedure result) process corresponding to at least one of the embodiments of the present disclosure. 11 is a flowchart illustrating a constraint condition registration process according to at least one of the embodiments of the present disclosure. 1 is a flowchart illustrating a system validation process according to at least one embodiment of the present disclosure. 1 is a conceptual diagram illustrating a format of specification verification result data according to at least one of the embodiments of the present disclosure. 1 is a flowchart illustrating a system comparison verification process according to at least one embodiment of the present disclosure. 11 is a conceptual diagram illustrating a format of specification comparison result data according to at least one of the embodiments of the present disclosure.

The following describes an embodiment of the present invention with reference to the drawings. Note that the following examples do not limit the invention according to 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 of the 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), an MPU (Micro Processing Unit), a GPU (Graphics Processing Unit), an FPGA (Field-Programmable Gate Array), etc.

Memory is a device that stores programs and data, such as 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 recording media such as a Hard Disc Drive (HDD), a Solid State Drive (SSD), a storage system, an Integrated Circuit (IC) card, a Secure Digital (SD) memory card, or an optical recording medium (such as a Compact Disc (CD) or a Digital Versatile Disc (DVD)).

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

The data management unit 10 manages the system specification 110, the specification verification result data 120, and the 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 viewed from the specification verification support device 1.

The system specification 110 includes formulated specification data corresponding to one or more information systems. The formulated specification data refers to data related to the specifications of an information system that is formulated as a single data structure according to a predetermined standard. The 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 formulated specification data 111 for system 1 and formulated specification data 112 for system 2. The system specification 110 may similarly include formulated 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 a number of models, where the events include events that occur in other models due to state transitions of a 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 the 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 that violates the state transition specification 111A specified by the event constraint 111B has occurred, and outputs the result as specification verification result data 120.

The specification comparison unit 40 prestores 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, the state transition specification 111A included in the system 1 formulated specification data 111 is compared 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 a predetermined standard. This makes it possible to mechanically perform the above-mentioned comparison. The specification comparison unit 40 outputs the comparison result, 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 a 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, a mouse, a touch panel, a card reader, and a voice input device.

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

The communication device is a wired or wireless communication interface that realizes 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 be configured to input and output information between it and 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 FIG. 2 corresponds to, for example, the system 1 formalized specification data 111 in FIG. 1. The formalized specification data represents the specifications of an information system based on at least multiple models and inter-model events.

A model corresponds to a single set of processes, such as "order receipt" in an electronic commerce system. A model includes 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 an instruction to ship a product to another processing unit, device, or system, is an event referred to here. Events include events that occur in other models due to the state transition of a model.

Event constraint data is data that specifies the violations that should be considered when an event occurs.

As conceptually shown in Figure 2, the specifications of an information system are formulated according to a predetermined standard that connects multiple models with inter-model events, making it easier to discover overlooked or missing aspects in the specifications. In addition, because the specification data formulated as described above is structured according to a unified standard, it becomes easy 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 of the embodiments of the present disclosure. In the following, each process described as being performed by the specification verification support device 1, the specification registration unit 20, the specification verification unit 30, or the specification comparison unit 40 may be performed mechanically by each processing unit, or may be performed by requesting user input from a user such as a person in charge as necessary, and using the information entered by the user.

The person in charge (human) describes the system specifications of the information system in a 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. The detailed processing of step S12 will be described later.

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

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

Figure 4 is a conceptual diagram illustrating a format of the formulated 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 FIG. 1, and the event constraint information corresponds to event constraint 111B in FIG. 1.

Event information has the following items: event name, business procedure name, model name, standard/exception category, and main/secondary category.

Model information has the model name as an item.

The state transition information has 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.

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

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

The specification registration unit 20 determines whether or not 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 the already existing model as the model that is 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 is a process required under normal circumstances (S27). If the event is a process that is always performed under normal circumstances, the process transitions to step S28, where the specification registration unit 20 determines the standard/exception classification of the event to be "standard." If the event is a process that is performed when an error occurs, or a process that is performed under normal circumstances but is not necessarily performed, the process 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 FIG. 6.

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

Note that it is not necessary to categorize events as main/secondary. If multiple events were to be interpreted as different types of events even when they merely change the state of some attributes of the 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 the model are managed as sub-events derived from main events. This makes it possible to prevent an increase in the 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, the process transitions to step S21 in FIG. 5, where the specification registration unit 20 extracts the next unprocessed event and processes it. If there are no unprocessed events, the process 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 an event registration (procedure result) process (S38). The specification registration unit 20 performs a constraint condition registration process (S39).

Details of steps S35 to S39 will be described later.

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

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

The specification registration unit 20 determines whether there is an unregistered event (S42). If there is an unregistered event, the process returns to step S41, where the specification registration unit 20 registers the next event. If there is no unregistered event, 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. In other words, 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 allows the person in charge to input or select the state transition of the model due to the event, and accepting user input, or by other means. 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 an event whose state transition is not registered (S44). If there is an event whose state transition is not registered, the process returns to step S43. If there is no event whose state transition is not registered, the process shown in FIG. 7 ends.

Figure 8 is a diagram showing an example of an event registration (standard) process corresponding to at least one embodiment of the present disclosure. The example shows a 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 certain events.

Five events were registered in the model (order) according to the flow shown in Fig. 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 an "Order Placed" event occurs in state S0, the state transition will be from S0 to S1. "E" in the state transition column means an error. For example, it is 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 state transition column is set to "E". The setting value "-" in the state transition column indicates that the state transition cannot occur in the first place.

Figure 9 is a flowchart illustrating an example of an event registration (exception) process corresponding to at least one embodiment of the present disclosure. Note that the event registration (exception) process 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 is an unregistered event (S52). If there is an unregistered event, the process returns to step S51, where the specification registration unit 20 registers the next event. If there is no unregistered event, 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 exception event. This determination process may be performed by the specification registration unit 20 outputting information to an output device such as a monitor that allows the person in charge to input or select the state transition of the model due to the event, and accepting user input, or by other means. 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 an event whose state transition is not registered (S54). If there is an event whose state transition is not registered, the process returns to step S53. If there is no event whose state transition is not registered, the process proceeds to step S55.

In step S55, the specification registration unit 20 determines whether or not 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 FIG. 9 ends.

In step S56, the specification registration unit 20 adds a state to the model and determines the state transition due to the event (standard).

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

As described above, the model (order) has six states: the initial state S0, the order state S1, the inventory confirmed state S2, the prepared for shipping state S3, the shipped state S4, and the completed state S5. The states transition depending on the occurrence of some event. Five standard events have already been registered in 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 Class: 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 state transition of the model, the addition is made (see step S56 in FIG. 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 column for state S6.

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

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

The specification registration unit 20 determines whether there is an unregistered sub-event (S62). If there is an unregistered sub-event, the process returns to step S61, where the specification registration unit 20 registers the next sub-event. If there is no unregistered sub-event, 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 allows the person in charge to input or select the state transition of the model due to the sub-event, and accepting user input, or by other means. 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 or not there is a sub-event whose transition destination (state transition) is not registered in the target model (S64). If there is a sub-event whose transition destination (state transition) is not registered, the process returns to step S63. If there is no sub-event whose transition destination (state transition) is not registered, the process 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 allows the person in charge to input or select the state transition of the secondary model due to the secondary event, and accepting user input, or by other means. 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 or not there is a sub-event whose transition destination (state transition) is not registered in the sub-model (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 FIG. 11 ends.

Figure 12 illustrates an example of event registration (sub-event) processing that corresponds 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 the 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 that were added to the target model were added to the sub-model.

Now, we will explain about sub-models. A sub-model means a model derived from a target model (main model). The specification registration unit 20 registers and manages state transitions for each model, so 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 specifies the transition by setting a sub-state derived from a specific state of the model (main model) as the state of the sub-model of the model. This prevents an explosive increase in the number of model types and reduces the processing load.

In the example shown in FIG. 12, the main model (order) has six states: initial state S0, received order state S1, inventory confirmed state S2, prepared for shipping state S3, shipped state S4, and completed state S5, and the states transition in response to the occurrence of some event. On the other hand, 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 the states transition in response to the occurrence of some 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" is also 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 detailed explanations 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 that the event that occurs is managed by the secondary model.

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

At the end of step S37 in FIG. 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 described (S72). If there are any lines where the procedure result has not been described, the process returns to step S71, where the specification registration unit 20 describes the next procedure result. If there are no lines where the procedure result has not been described, 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 the 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 is a state to add to the target model (S75). If there is a state to add, the process proceeds to step S76. If there is no state to add, the process shown in FIG. 13 ends.

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

Figure 14 illustrates an example of event registration (procedure result) processing that corresponds to at least one embodiment of the present disclosure.

In step S71, an entry is made in the procedure result column of the model "order". Entering means setting a set value. Here, the business procedure on the information system side when the event "preparing for shipment" occurs is inventory check. In reality, there is not always stock, so the procedure result of the business procedure is divided into two cases: when there is stock and when there is no stock. In addition, for the arrival of goods, in reality, there are cases where all the goods arrive and cases where only some of the goods arrive (other parts of the goods arrive at different times), so the procedure result is divided into two cases: when some goods arrive and when all goods arrive. In this way, when considering the specific business procedure at the time of the event occurrence, if the result of the procedure branches into two or more results, the event is divided. As an example shown in FIG. 14, the process of step S73 divided the event "preparing for shipment" of number 2 into four events of number 2, number 2-1, number 2-2, and number 2-3. Then, the procedure result and state transition are respectively determined and set as the set value.

In step S75, it is determined that a state of waiting for arrival needs to be added to the model "Order", so in step S76, state S11 (waiting for arrival) is added. The state transition due to existing events of the added state S11 (waiting for arrival) is set as the setting value. The existing events here refer to the events numbered 1 to 8, and also include the events numbered 2-1, 2-2, and 2-3 after 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 condition registration process corresponding to at least one embodiment of the present disclosure. The constraint condition registration process corresponds to step S39 in Figure 6.

The specification registration unit 20 registers event constraints (order of occurrence) (S81). More specifically, it registers in the system specifications 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 contradictions in the specifications.

The above event constraint that 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 may occur in an order different from the order specified in the first constraint in the state transition specification.

The specification registration unit 20 registers the event constraint (occurrence time) (S82). More specifically, the specific time when the event occurs 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 the time when an event occurs is referred to as the second constraint. In step S92 described below, the specification verification unit 30 checks whether an event can occur at a time in the state transition specification that is different from the time specified in the second constraint.

The specification registration unit 20 registers the event constraint (model CRUD) (S83). CRUD is a coined word made up of the initial letters of Create, Refer, Update, and Delete. 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 processing of the information system in response to the occurrence of an event for the target model. This makes it possible to extract an arrangement that is obviously irrational from the viewpoint of CRUD as a contradiction in the specification when multiple events are arranged in chronological order. For example, an arrangement of events in which information is referred to (R), updated (U), or deleted (D) when the information has not yet been created (C) is obviously irrational. Also, an arrangement of events in which information is referred to (R) or updated (U) after the information is deleted (D) is obviously irrational. When checking whether or not such an obviously irrational sequence of events exists, information from the registered CRUD is used.

That is, the model includes a model that generates, references, updates, or deletes information in response to the occurrence of an event. The above event constraint that 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 described below, 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 contents of the information to be registered are the same as those in step S83. In step S84, for the secondary model, the type of data to be created, referenced, updated, or deleted in the processing of the information system in response to the occurrence of an event is registered in the system specification 110.

That is, 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 described below, the specification verification unit 30 checks whether or not information is created, read, updated, or deleted in an order different from the order specified in the fourth constraint in the state transition specification.

FIG. 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 FIG. 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 is not specified 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 specifications 110. If an inconsistency based on the various event constraints registered by the specification registration unit 20 (see FIG. 15) is found in checking all combinations, 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.

Based on the output information indicating the inconsistencies, the person in charge corrects the inconsistencies. Based on the correction 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 a 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. The specification inconsistency information is used in the inconsistency output process of step S93. Figure 16 shows a format that expresses inconsistencies regarding state transitions from the specification inconsistency information.

The specification inconsistency information in the format shown in FIG. 17 has the following items: model 1, state name 1, model 2, state name 2, the name of the event that occurred, and the reason for the inability to transition. That is, when 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 event that occurred that caused the transition and the reason the state transition could not be made 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 item for model 1 or model 2 can be left blank, or the same model as that set for model 1 can be set for model 2.

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

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). The 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 modification 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. The system specification comparison is performed between the specifications of multiple systems based on the formalized specification data shown in FIG. 2. For example, the system 1 formalized specification data 111 and the system 2 formalized specification data 112 shown in FIG. 1 are compared. Note that the specifications of three or more types of systems may be compared simultaneously. The following will be described as an example of comparing the specifications of two types of systems.

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

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

The specification comparison unit 40 compares the state configurations (S113). More specifically, the list of states for each model is compared between the specifications of multiple systems. This comparison corresponds to a state configuration comparison in which, for each model present in the state transition specification, the list of states is compared with the model present in the comparison state transition specification corresponding to that model to extract excesses and deficiencies of states.

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

The specification comparison unit 40 compares the constraints (S115). More specifically, it compares the list 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 in a format that conforms to predetermined standards as the above-mentioned formalized specification data. Therefore, the specification comparison unit 40 can mechanically perform the above-mentioned comparison between the specifications of multiple systems.

The above-mentioned comparison of constraints corresponds to a constraint comparison in which a comparison event constraint, which is an event constraint corresponding to a comparison state transition specification, is stored in advance, and the specification comparison unit 40 compares a list of violations between the event constraint corresponding to the state transition specification and the comparison event constraint to extract the excess or deficiency of violations.

Figure 19 is a conceptual diagram illustrating a 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 of each piece of information and the format of the information shown in FIG. 19 are merely examples, and a person skilled in the art may set the classification and format according to the content of the specification comparison result to be obtained as appropriate.

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).

The 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 item "Name of the system that does not have it" is handled in the same way for other difference information described below, so a detailed explanation will be omitted from here on to avoid duplication.

The 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.

The difference information (state configuration comparison) includes the model name, state name, and the name of the system that does not have the item.

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 means the state (state name) of the transition destination.

The 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. The 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. Those skilled in the art can 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 that supports specification verification of an information system has a specification registration unit 20 that accepts registration of state transition specifications 111A that specify 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 transitions of the models, and event constraints 111B that specify violations that should be violated when the events occur. The specification verification support device 1 has a specification verification unit 30 that verifies whether any event that corresponds to a violation has occurred in the state transition specifications 111A. In this way, the state transition specifications that include events that occur in other models due to the state transitions of the models are registered, and in the verification of the system specifications, it is checked whether any event that corresponds to a violation has occurred according to the state transition specifications, thereby reducing oversight of errors in the system specifications.

The specification verification support device 1 further includes a specification comparison unit 40 that prestores 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. This makes it possible to present differences by comparing with, for example, a state transition specification of a proven information system of the same type, and to assist in discovering errors in the system specifications.

The specification comparison unit 40 executes 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 excess or deficiency of 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 the model to extract excess or deficiency of 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 the model to extract excess or deficiency of states; and a transition destination comparison that compares the transition destination states for corresponding events for each model in the state transition specification 111A with the model in the comparison state transition specification corresponding to the model to extract differences in the transition destinations. This makes it possible to compare models in the state transition specification and the comparison state transition specification to present the differences and assist in finding errors in each model in the system specifications.

A comparison event constraint, which is an event constraint corresponding to the comparison state transition specification, is further stored in advance. The specification comparison unit 40 further performs a constraint comparison to compare a list of violations between the event constraint corresponding to the state transition specification 111A and the comparison event constraint, and extracts excesses and deficiencies of violations. This makes it possible to present event violations between the state transition specification and the comparison state transition specification, and to assist in discovering errors related to the event constraints of 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 can occur in an order different from the order specified in the first constraint in the state transition specification 111A. 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 the time when the event occurs. 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 time when the event occurs.

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 models. 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 specifies transitions in which secondary states derived from a specific state of a model are treated as states of sub-models of the model. This makes it possible to prevent an explosive increase in the number of combinations of model states and events in state transition specifications that include events between models.

The sub-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 sub-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 sub-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 of states that are added as a result of the event being split into multiple events and state transitions related to the added states in the state transition specification 111A. This makes it possible to support the registration of state transition specifications that can execute verification of system specifications including 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 having a processor and memory accepts registration of state transition specifications 111A that prescribe 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 transitions of the models, and event constraints 111B that prescribe violations that should be violated when the events occur, and verifies whether any events that fall under the violations in the state transition specifications 111A have occurred. In this way, a state transition specification that includes events that occur in other models due to the state transitions of a model is registered, and in verifying the system specifications, it is checked whether any events that fall under the violations in the state transition specifications have occurred, thereby reducing oversight of errors in the system specifications.

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 for 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 111B that specify violations that should be violated when the events occur, and to verify whether any events that fall under the 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 transitions of a model, and checks whether any events that fall under the violations in the state transition specifications have occurred in the verification of the system specifications, thereby reducing oversight of errors in the system specifications.

Reference Signs List 1: specification verification support device, 10: data management section, 20: specification registration section, 30: specification verification section, 40: specification comparison section

Claims (12)

A specification verification support device for supporting specification verification of an information system, comprising:
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 state transition specifications including events that occur in other models due to state transitions of the models, and event constraints that define violations that should be violated 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 verification support device having the above configuration. a specification comparison unit that prestores 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 a difference;
2. The specification verification support device according to claim 1. The specification comparison unit is
a model configuration comparison for extracting an excess or deficiency of models by comparing a list of models in the state transition specification with a list of models in the comparison state transition specification;
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 extracting excess or deficiency of states by comparing a list of states of each model in the state transition specification with a model in the comparison state transition specification corresponding to the model;
A transition destination comparison for extracting a difference in the transition destinations by comparing, for each model in the state transition specification, a model in the comparison state transition specification corresponding to the model and a transition destination state for a corresponding event;
Execute at least one of the following:
3. The specification verification support device according to claim 2. A comparison event constraint which is an 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.
3. The specification verification support device according to claim 2. the event constraints include a first constraint that specifies an order of occurrence of a plurality of events;
the specification verification unit checks whether or not events may occur in an order different from an order defined in the first constraint in the state transition specification;
2. The specification verification support device according to claim 1. the event constraint includes a second constraint that specifies when the event occurs;
the specification verification unit confirms whether or not an event occurs at a time different from a time defined in the second constraint in the state transition specification.
2. The specification verification support device according to claim 1. The model includes a model for generating, referencing, updating, or deleting information in response to an occurrence of an event;
the event constraints include a third constraint that specifies an 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 an order defined in the third constraint in the state transition specification;
2. The specification verification support device according to claim 1. The state transition specification defines a transition in which a sub-state derived from a specific state of a model is a state of a sub-model of the model.
2. The specification verification support device according to claim 1. The sub-model includes a model that generates, references, updates, or deletes information in response to an event occurrence;
The event constraints include a fourth constraint that specifies an order of creating, reading, updating, and deleting information by the secondary model;
the specification verification unit checks whether or not information is created, read, updated, or deleted in an order different from an order defined in the fourth constraint in the state transition specification;
9. The specification verification support device according to claim 8. the specification registration unit, when a plurality of procedure results exist in a business procedure corresponding to an event to a model, 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;
2. The specification verification support device according to claim 1. A specification verification support method for supporting specification verification of an information system, comprising:
1. An apparatus comprising a processor and a memory,
A state transition specification is provided for each of a plurality of models, the state transition specification defining an event-induced state transition, the event including an event that occurs in another model due to the state transition of the model, and an event constraint is provided for each of the events, the event constraint defining a violation that should be considered as a violation when the event occurs;
Verifying whether or not an event corresponding to the violation in the state transition specification occurs;
A specification verification support method that performs the above. A specification verification support program for supporting specification verification of an information system, comprising:
An apparatus having a processor and a memory,
A state transition specification is provided for each of a plurality of models, the state transition specification defining an event-induced state transition, the event including an event that occurs in another model due to the state transition of the model, and an event constraint is provided for each of the events, the event constraint defining a violation that should be considered as a violation when the event occurs;
Verifying whether or not an event corresponding to the violation in the state transition specification occurs;
A specification verification support program to help you do this.

Images