JP5774468B2 - State transition table generator - Google Patents

Description

  Embodiments described herein relate to a state transition table generation device.

  In recent years, as software has become more complex, it is easier to introduce specification errors than ever before, and it is becoming difficult for humans to verify the specifications. As a solution, model checking, which is one of the formal methods, has attracted attention, and practical application of model checking is also progressing, and non-conforming cases that are difficult to detect by human hands have been found and are effective.

  However, in order to use the model checker, which is a device that performs the model check, specialized skills and know-how are required. Therefore, in order to facilitate the introduction of model checking more efficiently, a support tool has been developed that can automatically generate and check a model checker-specific language from specifications such as state transition diagrams, state transition tables, and flowcharts. Has been.

JP 2007-11605 A JP 2008-198103 A

  Conventional support tools support only specific expressions (figure or specification information) as input information. Therefore, usage restrictions are imposed depending on what type of input specification is supported by the support tool to be used. For example, when the specifications are mainly described in a flowchart, there is a problem that support software based on a state transition diagram / state transition table cannot be used.

  An object of the present invention is to create a state transition table corresponding to a specification described in a time-series order format such as a flowchart. The result of model checking using the state transition table corresponds to the flowchart. It is in the point that it is possible to maintain the relationship and easily find a specification error.

According to one embodiment, a state transition table generation device is proposed. This state transition table generation device has a first generation unit and a second generation unit.
The first generation means attaches information for specifying an event and an action to conditional branching and processing in data representing an input / output order series specification, and specifies information for specifying an action execution path state in a single path without branching. In addition, there is one record for one action execution path state, and each record generates a state definition record table which is information including an event, a previous event, and an action sequence.

  The second generation means has one record for each action execution path state included in the state definition record table based on the state definition record table, and each record is included in each state definition record table. A state transition table that is information having fields corresponding to events is generated.

The figure which showed the flow of the model check using the state transition table production | generation apparatus and the state transition table output by this state transition table production | generation apparatus Functional block diagram showing a configuration example of the state transition table generation device Flow chart showing an example of status definition record table generation processing The flowchart which showed the example of the state definition record table production | generation process following FIG. 3A Flowchart that is the input / output sequence specification that is the source of the status definition record The figure which showed the example of the state definition record table produced | generated from the process target flowchart of FIG. Flow chart showing an example of state transition table generation processing The figure which shows an example of the state definition record table which the state definition record table production | generation part of this Embodiment produced | generated The figure which showed the process which completes the state transition table shown in FIG. FIG. 8 is a diagram showing a process of completing the state transition table shown in FIG. 17 following FIG. FIG. 9 is a diagram showing a process of completing the state transition table shown in FIG. 17 following FIG. FIG. 10 is a diagram showing a process of completing the state transition table shown in FIG. 17 following FIG. The figure which showed the process in which the state transition table shown in FIG. 17 is completed following FIG. FIG. 12 is a diagram showing a process of completing the state transition table shown in FIG. 17 following FIG. The figure which showed the process of completing the state transition table shown in FIG. 17 following FIG. FIG. 14 is a diagram showing a process of completing the state transition table shown in FIG. 17 following FIG. FIG. 15 is a diagram showing a process of completing the state transition table shown in FIG. 17 following FIG. The figure which shows the example of the state transition table which the state transition table production | generation part of this Embodiment produced | generated based on the state definition record table shown in FIG. The figure which shows an example of the state definition record table produced | generated from the flowchart of FIG. 17 by performing a state definition record table production | generation process The figure which shows the example of the state transition table produced | generated from the state definition record of FIG. 18 by the state transition table production | generation process Figure showing an example of "event / action definition record" The figure which shows an example of the source code used as the input of the state transition table generation device The figure which shows the state where the label of the event and action was attached | subjected to the source code of FIG. The figure which shows the example of the state definition record table obtained as a result of executing the state definition record table generation processing (see FIG. 3) The figure which shows the example of the state transition table obtained as a result of performing a state transition table production | generation process (refer FIG. 6) based on the state definition record table shown in FIG. The block diagram which shows the structural example of the state transition table production | generation apparatus concerning 2nd Embodiment The flowchart which shows an example of the state definition record production | generation process which is operation | movement of a state definition record production | generation part Flowchart following FIG. The figure which shows the flowchart which is the input / output order series specification which becomes the origin of the said state definition record table in this specific example The figure which showed the example of the state definition record table produced | generated from the process target flowchart of FIG. The figure which shows the example of the state transition table produced | generated from the data of the state definition record table shown in FIG. Sequence diagram showing an example of processing for assigning IP addresses The figure which shows the example of the processing flowchart of PC-1 which is a client The figure which shows the flowchart of FIG. 32 to which the state name (action execution path state) was attached | subjected. A diagram showing the state transition table generated by the state transition table generating device from the flowchart (input / output sequence specification 10) in the state transition diagram The figure which shows the example of the process flowchart of PC-3 which is a DHCP server. The figure which shows the flowchart of FIG. 35 to which the state name (action execution path state) was attached | subjected. The state transition table generated by the state transition table generating device from the flowchart (input / output order sequence specification 10) of FIG. 32 is shown in the state transition diagram.

Hereinafter, a state transition table generating device according to an embodiment of the present invention will be described with reference to the drawings.
[First embodiment]

FIG. 1 is a diagram illustrating a flow of model checking using a state transition table generation device according to the first embodiment and a state transition table output by the state transition table generation device.
A user (or an operator, etc., who is the same hereinafter) who performs model checking first prepares an input / output order sequence specification. Here, the “input / output order sequence specification” refers to a specification written in a time-series order format, such as a flowchart.

The user inputs the input / output order sequence specification 10 to the state transition table generation device 11. The state transition table generation device 11 processes the data of the input / output order sequence specification 10 by the state transition table generation processing method, and generates and outputs the state transition table 12 as the processing result.
The user creates a test code 13 based on the state transition table 12 and creates a test formula 14. The user inputs the inspection code 13 and the inspection formula 14 to the model checker 15.

  The model checker 15 executes a model check process and outputs a counterexample 16. By analyzing the counterexample, the user finds a problem, corrects the inspection code 13, and further inspects the corrected inspection code 13 by the model inspector 15 so as to crush the problem. The code 13 is improved.

  FIG. 2 is a functional block diagram illustrating a configuration example of the state transition table generation device 11. 2 are elements in which the state transition table generation device 11 is regarded as a group for each function, and the actual state transition table generation device 11 has hardware (circuitry) corresponding to each configuration aspect. , Modules, units, etc.) are not required.

  The state transition table generation device 11 is a device realized by an information processing device such as a computer or a workstation. The information processing apparatus includes an arithmetic processing unit (CPU), a main memory (RAM), a read-only memory (ROM), an input / output device (I / O), and, if necessary, an external storage device such as a hard disk device. It is a device.

  The state transition table generation device 11 includes an input / output order sequence specification storage unit 21, a state definition record table generation unit 22 corresponding to the first generation unit of the present embodiment, and a first generation unit of the present embodiment. A state transition table generation unit 23 corresponding to the above and an event / action definition record table generation unit 24. The input / output order sequence specification storage unit 21 is connected to the state definition record table generation unit 22, the state definition record table generation unit 22 is connected to the state transition table generation unit 23, and the event / action definition record table generation unit Reference numeral 24 denotes a state transition table generation unit 23. Here, “connected” means that data, information, instructions, etc. can be exchanged, and is not limited to physical connections such as being connected by wiring.

  The input / output order sequence specification storage unit 21 has a function of storing input / output order sequence specifications input by the user. The input / output order sequence specification may be stored as any data as long as it can be read by the state definition record table generation unit 22.

  The state definition record table generation unit 22 receives data representing the input / output order sequence specification from the input / output order sequence specification storage unit 21, and executes the state definition record table generation process described later, thereby representing the state definition record table. Has the function of generating and outputting.

  The state transition table generation unit 23 receives data representing the state definition record table from the state definition record table generation unit 22 from the state definition record table generation unit 22, and executes a state transition table generation process to be described later. Has a function of generating and outputting data representing.

  The event / action definition record table generation unit 24 is an event / data that is a data in which a label (code) attached to an event and an action included in the input / output order series specification is associated with a sentence or a word indicating the content of the label. It has a function to generate and store an action definition record table.

[Status definition record table generation processing]
Hereinafter, an example of the state definition record table generation process will be described with reference to FIGS. 3A and 3B. FIG. 3A is a flowchart showing an example of state definition record table generation processing, and FIG. 3B is a flowchart following FIG. 3A. In this description, the input / output order sequence specification 10 is described as a flowchart.

  First, the state definition record table generating unit 22 assigns an event and an action number to each element of conditional branching and processing in the flowchart (S10). That is, event numbering is performed for conditional branch processing, and action numbering is performed for actions (normal processing).

  Next, the state definition record table generation unit 22 generates a state definition record table. The state definition record table has one record for one action execution path state, and each record is information having three fields of “event”, “previous event”, and “action series”. When the state definition record table generation unit 22 reads “Start” that is the first element of the flowchart, the state definition record table generation unit 22 stores “State0” in the action execution path state column and the event name “Start” in the event column. Is added to the state definition record table (S20).

Next, the state definition record table generating unit 22 determines whether all elements other than “End” have been read and the state has been defined (S30). When all the elements other than “End” have been read, the state definition record table generation unit 22 stores the state name including the current number of states in the action execution path state column and also in the event column. A new state definition record storing “End” is generated and added to the state definition record table (S110).
Next, the state definition record table generation unit 22 registers an event of a record that defines a state immediately before the two records as an event before a registered or registered event (S120).
On the other hand, when all elements other than “End” have not been read (No in S30), the state definition record table generating unit 22 reads one element from the connected portion of the flowchart (S40).

  Next, the state definition record table generating unit 22 determines whether or not the read element is a conditional branch (S50). When it is determined that the element is not a conditional branch (S50, No), the state definition record table generating unit 22 uses the element (processing) as an action for the event of the condition, and also reads the element number (also referred to as a label) of the element. ) Is registered in the state definition record table (S60). Then, it returns to step S30 mentioned above and continues a process.

On the other hand, when it is determined in step S50 that the element is a conditional branch (S50, Yes), the state definition record table generation unit 22 registers a state name that defines a state caused by the conditional branch in the state definition record table. (S70). Here, the “state” is an action execution path and corresponds to a path (path) on the flowchart from a certain conditional branch to the next conditional branch. In this example, the state name is described in the format “State [number of state records]”.
In this example, the above route is treated as a state, but it can be implemented even if each conditional branch is treated as a state. In this case, the route is not related to state distinction.

  Next, the state definition record table generation unit 22 determines whether or not the conditional branch has been registered in the state definition record table as an event (S80). When it is determined that the conditional branch has not been registered in the state definition record table as an event (S80, No), the state definition record table generation unit 22 creates two new state definition records in the state definition record table, The event corresponding to “TRUE” of the conditional branch is registered in the event field of one record, and the event corresponding to “FALSE” of the conditional branch is registered to the other record (S90).

  Next, the state definition record table generation unit 22 registers the event of the record that has defined the state immediately before the two records in the event before the registered or registered event (S100). Thereafter, the process returns to step S30 to continue the processing.

On the other hand, if it is determined in step S80 that the conditional branch has already been registered in the state definition record table as an event (S80, Yes), the state definition record table generation unit 22 executes step S100 without performing step S90. To do.
This is the end of the description of the state definition record table generation process.

[Concrete example]
A specific example of the state definition record table generation process will be described. FIG. 4 is a flowchart (referred to as a “processing target flowchart”) that is the input / output order sequence specification 10 that is the basis of the state definition record table in this specific example. FIG. 5 is a diagram showing an example of a state definition record table generated from the process target flowchart of FIG. Hereinafter, a specific example of the state definition record table generation process will be described with reference to FIGS. 3, 4, and 5.

  The contents of the processing target flowchart are as follows. First, there is step S101 which is the first conditional branch. There is step S102 which is an action corresponding to “True” in the conditional branch step S101, and there is step S102 which is another action following step S102. The action corresponding to “False” in the conditional branch step S101 is step S103.

  Following step S103 is step S104, which is the second conditional branch. As an action corresponding to “True” in the conditional branching step S104, there is Step S105 which is an action. After Step S105, the processing of the processing target flowchart reaches “End”. Also, “End” corresponds to “False” in step S104 of the second conditional branch.

  Now, a state definition record table creation process is performed based on this process target flowchart. First, the state definition record table generation unit 22 assigns an event and an action number to each element of conditional branching and processing in the flowchart (FIG. 3, S10). Specifically, an event number “E1” is assigned to the first conditional branch S101, and an event number “E2” is assigned to the second conditional branch S104. Action numbers “A1”, “A2”, and “A3” are assigned to actions S102, S103, and S104, respectively.

  Next, the state definition record table generation unit 22 generates a state definition record table, and [State0] is stored in the action execution path state column as the first record of the state definition record table, and [Start] ] Is stored (FIG. 3, S20).

  Next, the state definition record table generation unit 22 determines whether all elements other than “End” have been read and the state has been defined (S30 in FIG. 3). In this specific example, since no element has been read yet, the determination is “No” and the process proceeds to step S40.

Next, the state definition record table generation unit 22 reads one element from the connected portion of the processing target flowchart (S40 in FIG. 3). In this example, the element “Start” of the processing target flowchart is read.
Next, the state definition record table generating unit 22 determines whether or not the read element is a conditional branch (FIG. 3, S50). In this example, it is determined that the element “Start” is not a conditional branch (FIG. 3, S50, No).

  Next, the state definition record table generation unit 22 registers the element number of the read element in the state definition record table as an action for the event of the condition (process) (FIG. 3, S60). Specifically, “State0” is described in the “Action execution path status” field in the first line of the state definition record table shown in FIG. 5, and the element number of the element read in the “Event” field in the first line “Start” is described.

Next, the state definition record table production | generation part 22 reads the next one element from the connection part of a process target flowchart after determination of step S30 (FIG. 3, S40). In this example, the element “E1” of the processing target flowchart is read.
Next, the state definition record table generation unit 22 determines whether the read element is a conditional branch. In this example, the element “E1” is determined to be a conditional branch (FIG. 3, S50, Yes).

  Next, the state definition record table generation unit 22 determines a state name that defines a state caused by the conditional branch (FIG. 3, S70). In this example, the state definition record table generation unit 22 determines a route (route from E1 to E2 via A1, A2) as the state name “State1” in “True” of the conditional branch “E1”. A path in “False” of the branch “E1” (path from E1 to E2 via A2) is defined as a state name “State2”.

  Next, the state definition record table generation unit 22 determines whether or not the conditional branch has been registered in the state definition record table as an event (S80 in FIG. 3). In this example, it is determined that the conditional branch “E1” has not yet been registered in the state definition record table (FIG. 3, S80, No), and the process proceeds to step S90.

  In step S90, the state definition record table generating unit 22 creates two new state definition records in the state definition record table, and registers an event corresponding to “True” in the conditional branch in the event field of one record. In the other record, an event corresponding to “False” of the conditional branch is registered. In this example, the state definition record table generation unit 22 creates the second row and the third row in the state definition record table of FIG. 5 and describes “State1” in the “action execution path state” column of the second row. In addition, describe “E1 [True]” in the “Event” column. Furthermore, the state definition record table generating unit 22 describes “State2” in the “action execution path state” field in the third row and “E1 [False]” in the “event” field.

  Next, the state definition record table generation unit 22 registers an event of a record that defines a state immediately before the two records as an event before a registered or registered event (FIG. 3, S100). In this example, the state definition record table generation unit 22 “previous event” corresponding to “E1 [True]” (second line) and “E1 [False]” (third line), which are the events registered immediately before. In the column, the event “Start” described in the “Event” column of the record (first line) in which the state has been defined immediately before is described.

Next, the state definition record table generating unit 22 returns to step S30 and then reads the element “A1” next to the element “E1” in step S40 (FIG. 3, S40).
Next, the state definition record table generation unit 22 determines whether the read element is a conditional branch. In this example, it is determined that the element “A1” is not a conditional branch (FIG. 3, S50, No).

  Next, the state definition record table generation unit 22 registers the element number of the read element in the state definition record table as an action for the event of the condition (process) (FIG. 3, S60). Specifically, “A1” is described in the “action series” column of the second row of the state definition record table shown in FIG.

Next, the state definition record table generating unit 22 returns to step S30, and then reads the element “A2” next to the element “A1” in step S40 (FIG. 3, S40).
Next, the state definition record table generating unit 22 determines whether or not the read element is a conditional branch (FIG. 3, S50). In this example, it is determined that the element “A2” is not a conditional branch (FIG. 3, S50, No).

  Next, the state definition record table generation unit 22 registers the element number of the read element in the state definition record table as an action for the event of the condition (process) (FIG. 3, S60). Specifically, it is described so that “A2” is added to the “action series” column in the second row of the state definition record table shown in FIG.

Next, the state definition record table generating unit 22 returns to step S30, and then reads the element “E2” next to the element “A2” in the process target flowchart in step S40 (FIG. 3, S40).
Next, the state definition record table generating unit 22 determines whether or not the read element is a conditional branch (FIG. 3, S50). In this example, the element “E2” is determined to be a conditional branch (FIG. 3, S50, Yes).

  Next, the state definition record table generation unit 22 determines a state name that defines a state caused by the conditional branch (S70). In this example, the state definition record table generating unit 22 defines a route in “True” of the conditional branch “E2” (a route from E2 to End via A3) as the state name “State3” and the conditional branch “E3”. A path (path from E2 to End) in “False” of “E2” is defined as a state name “State4”.

  Next, the state definition record table generation unit 22 determines whether or not the conditional branch has been registered in the state definition record table as an event (S80 in FIG. 3). In this example, it is determined that the conditional branch “E2” has not yet been registered in the state definition record table (FIG. 3, S80, No), and the process proceeds to step S90.

  In step S90, the state definition record table generation unit 22 adds two new state definition records to the state definition record table shown in FIG. 5, and sets an event corresponding to “True” in the conditional branch as an event of one record. Register in the field and register the event corresponding to “False” of the conditional branch in the other record. In this example, the state definition record table generation unit 22 creates the fourth and fifth rows in the state definition record table, describes “State3” in the “action execution path state” column of the fourth row, and “event” "E2 [True]" is written in the "" column. Furthermore, the state definition record table generating unit 22 describes “State4” in the “action execution path state” column of the fifth line and “E2 [False]” in the “event” column.

  Next, the state definition record table generation unit 22 registers an event of a record that defines a state immediately before the two records as an event before a registered or registered event (FIG. 3, S100). In this example, the state definition record table generation unit 22 records “E1” described in the event column of the record (records corresponding to the second and third rows) registered immediately before the registration of the fourth and fifth rows. “True” ”(second line) and“ E1 [False] ”(third line) are described in the“ previous event ”column of the fourth and fifth lines.

Next, the state definition record table generating unit 22 returns to step S30 and then reads the element “A3” next to the element “E2” in step S40 (FIG. 3, S40).
Next, the state definition record table generating unit 22 determines whether or not the read element is a conditional branch (FIG. 3, S50). In this example, it is determined that the element “A3” is not a conditional branch (S50, No).

  Next, the state definition record table generation unit 22 registers the element number of the read element in the state definition record table as an action for the event of the condition (process) (FIG. 3, S60). Specifically, “A3” is described in the “action series” column of the fourth row of the state definition record table shown in FIG.

  Next, the state definition record table generating unit 22 returns to step S30 and determines whether all elements other than the end (End) have been read (S30). In this example, the state definition record table generation unit 22 determines that all elements other than the end (End) have been read (S30, Yes), and proceeds to step S110 in FIG. 3B.

  In step S110, the state definition record table generation unit 22 stores a state name including the current number of states in the action execution path state column, and generates a new state definition record in which “End” is stored in the event column. It adds to the definition record table (S110). In this example, it corresponds to the record in the sixth row.

Next, the state definition record table generation unit 22 registers an event of a record that defines a state immediately before the two records as an event before a registered or registered event (S120). In this example, the state definition record table generation unit 22 “E2 [True]” described in the event column of the record (records corresponding to the fourth and fifth lines) registered immediately before the registration of the sixth line. (Fourth line) and “E2 [False]” (Fifth line) are described in the “Previous event” column of the sixth line. The state definition record table based on the flowchart shown in FIG. 4 is completed.
This is the end of the description of the state definition record table generation process.

[State transition table generation processing]
Next, state transition table generation processing, which is processing for generating a state transition table from a state definition record table, will be described. FIG. 6 is a flowchart illustrating an example of the state transition table generation process. Hereinafter, the state transition table generation process will be described with reference to this flowchart.

The state transition table generation unit 23 that has acquired the state definition record table generated by the state definition record table generation unit 22 uses the contents described in the “action execution path state” column of the state definition record table for each row of the state transition table. In the state transition table, the contents described in the “event” column of the state definition record table are described in the state transition table as indexes of each column (S201).
Next, the state transition table generating unit 23 reads the first state definition record (corresponding to the first row of the state definition record table) of the state definition record table (S202).

  Next, the state transition table generation unit 23 determines whether or not all the state definition records in the acquired state definition record table have been read (S203). When it is determined that all the state definition records have been read (S203, Yes), the state transition table generating unit 23 stores predetermined information indicating that all the empty cells in the state transition table are blank, for example, the symbol “ / "(Slash) is written (step S211). After step S211, the state transition table generation unit 23 ends the state transition table generation process. On the other hand, if it is determined in step S203 that all the state definition records have not been read (S203, No), the state transition table generation unit 23 determines that the state definition record currently being processed (hereinafter referred to as “processing target record”). It is determined whether or not the information described in the “action execution path state” column is “State 0” (S204).

  When it is determined in step S204 that the description in the “action execution path state” field of the processing target record is “State0” (No in S204), the state transition table generating unit 23 sets the next state definition record as the processing target record. (S205). Thereafter, the process returns to step S203.

  On the other hand, when it is determined in step S204 that the “action execution path state” of the processing target record is not “State0” (S204, Yes), the state transition table generating unit 23 reads the processing target record (S206).

  The state transition table generation unit 23 determines whether any event is described in the “previous event” column of the processing target record read in S206 (S207). In step S207, when it is determined that no event is described in the “previous event” column (S207, No), the state transition table generation unit 23 determines the action execution path state for the previous event as “State0”. (S208). This “State 0” is used as information for determining a “processing target cell” to be described later.

  After step S208 is executed, the state transition table generation unit 23 extracts a state definition record group having an action execution path state for the previous event from the state definition record table (S209). More specifically, the state transition table generation unit 23 selects the same event as the event described in the “previous event” column of the processing target record among all the state definition records in the state definition record table. Extract all the state definition records in This extracted line is called an extracted record. Further, when there is no description in the “previous event” column in the processing target record, the “Init” row in the state transition table is a row for defining the processing target cell.

Next, the state transition table generating unit 23 defines an action execution path state for the event as a state transition destination of the event for the action execution path state group for the previous event (S210). More specifically, the state transition table generating unit 23 includes, in the state transition table, the “action execution path state” field of the state definition record having the event described in the “previous event” in the processing target record in the “event” field. A cell (referred to as a processing target cell) that is an intersection of a row having an index that matches the action execution path state described in the column and a column having an index that matches the event described in the “event” column of the processing target record In the status column, the action execution path status described in the “action execution path status” column of the processing target record is written. If there is a description of an action in the “action series” column of the processing target record, the action is written in the action column of the processing target cell.
After step S210 is completed, the state transition table generation unit 23 returns to step S205.

On the other hand, if it is determined in step S207 described above that an event is described in the “previous event” field (S207, Yes), the state transition table generation unit 23 immediately proceeds to step S209.
This is the end of the description of the state transition table creation process.

[Specific example of state transition table creation processing]
Next, the state transition table creation process described above will be described with a specific example. FIG. 7 is a diagram illustrating an example of the state definition record table generated by the state definition record table generation unit 22 according to the present embodiment. FIG. 17 illustrates the present embodiment based on the state definition record table illustrated in FIG. It is a figure which shows the example of the state transition table which the state transition table production | generation part 23 of the form produced | generated. 8 to 16 are diagrams showing a process of completing the state transition table shown in FIG. In the following, how the state transition table shown in FIG. 17 is generated from the state definition record table shown in FIG. 7 by the state transition table creation processing will be described with reference to FIGS.

  The state transition table generation unit 23 that has acquired the state definition record table generated by the state definition record table generation unit 22 displays the “action execution path state” column (each cell in the leftmost column) of the state definition record table of FIG. “State0”, “State1”, “State2”, “State3”, “State4”, “State5”, and “Init” in addition to these are described in each cell in the leftmost column of the state transition table. "Start", "E1 [true]", "E1 [false]", "Contents" described in the "Event" column (each cell in the second column from the left end) in the state definition record table “E2 [true]”, “E2 [false]”, and “End” are described as the index of each column in each cell in the top row of the state transition table (see S201 in FIG. 6).

  Next, the state transition table generation unit 23 reads the state definition record in the first row of the state definition record table (S202 in FIG. 6). The state definition record in the first row is the “processing target record” at this point. 8 is a diagram illustrating an example of a state transition table before states and events are described as indexes, and FIG. 9 is a diagram illustrating a state in which states and events are described as indexes in the state transition table of FIG. is there.

  Next, the state transition table generation unit 23 determines whether all the state definition records in the state definition record table have been read (S203 in FIG. 6). In this specific example, the state transition table generation unit 23 determines that all rows have not been read (No in FIG. 6, S203).

  Next, the state transition table generation unit 23 determines whether or not the information described in the “action execution path state” cell of the processing target record is “State 0” (FIG. 6, S204). In this specific example, the state transition table generation unit 23 determines that the information described in the cell in the “action execution path state” column in the processing target record in step S203 is “State0”, and proceeds to step S205 (S204, No). Here, the state transition table generating unit 23 includes a line in which “Init” is described in the action execution path state and a column having an index that matches the event “Start” described in the “event” column of the processing target record. The action execution path state “State0” described in the “action execution path state” column of the processing target record is written in the state column of the cell that is the intersection (referred to as the processing target cell). FIG. 10 shows an example of a state transition table in which “State 0” is written in the above process after the state of FIG.

[State definition record table, second row processing]
In step S205, the state transition table generating unit 23 sets the next record in the state definition record table as a process target record (S205 in FIG. 6). In this specific example, the state definition record whose cell in the “Action Execution Path State” column in the second row of the state definition record table of FIG. 7 is “State1” is determined as a new process target record.

  Next, the state transition table generation unit 23 determines whether or not all the rows (records) in the acquired state definition record table have been read (S203 in FIG. 6). In this specific example, the state transition table generation unit 23 determines that all rows have not been read (No in FIG. 6, S203).

  Next, the state transition table generation unit 23 determines whether or not the information described in the “action execution path state” cell of the processing target record in the state definition record table is “State0” (FIG. 6, S203). In this specific example, since the “action execution path state” cell of the processing target record is “State 1”, the process proceeds to step S206. In step S206, the state transition table generating unit 23 reads the processing target record. In this specific example, a state definition record in which the cell in the “action execution path state” column in the second row of the state definition record table is “State1” is read.

  Next, the state transition table generation unit 23 determines whether there is an event described in the “previous event” column in the processing target record (S207 in FIG. 6). In this specific example, since there is a description of the event “Start” in the “previous event” column in the second row of the state definition record table, the process proceeds to step S209.

  The state transition table generation unit 23 extracts a state definition record group having an action execution path state for the previous event from the state definition record table (S209 in FIG. 6). The extracted record group is called an “extracted record group”. In this specific example, the state definition record in which the event “Start” is described in the “event” column in the state definition record table is extracted, and the extracted record group is only the state definition record in the first row.

  Next, the state transition table generation unit 23 creates a row having an index that matches the action execution path state described in the “action execution path state” column of the extracted record group in the state transition table, and “event” of the processing target record. The action execution described in the “action execution path status” column of the processing target record in the status column of the cell (referred to as the processing target cell) that intersects with the column having the index matching the event described in the “” column Although the path state is written (S210 in FIG. 6), the action execution path state described in the “action execution path state” column of the first line which is the extracted record is “State0”. Further, the event described in the “event” column of the processing target record is “E1 [True]”. Therefore, the processing target cell in the state transition table is determined to be a cell that is the intersection of the second row with “State 0” as an index and the second column from the left end with “E1 [True]” as an index. The state transition table generation unit 23 writes the action execution path state “State1” described in the “action execution path state” field of the processing target record in the state column (upper side of the cell) of the processing target cell. Further, the state transition table generation unit 23 sets the action “A1, A2” described in the “action series” column of the processing target record in the action column (lower side of the cell) of the processing target cell. Write to (lower side in the cell) (see S210 in FIG. 6). FIG. 11 shows an example of a state transition table in which the state “State1” and the actions “A1, A2” are written in the processing target cell.

[State definition record table, third row processing]
Next, the state transition table generation unit 23 proceeds to step S205, and sets the next record in the state definition record table as a process target record (FIG. 6, S205). In this specific example, the state definition record in which the cell in the “action execution path state” column in the third row of the state definition record table of FIG. 5 is “State2” is determined as a new processing target record.

  Next, the state transition table generation unit 23 determines whether or not all the rows (records) in the acquired state definition record table have been read (S203 in FIG. 6). In this specific example, the state transition table generation unit 23 determines that all rows have not been read (S203, No).

  Next, the state transition table generation unit 23 determines whether or not the information described in the cell of the process target record “action execution path state” in the state definition record table is “State 0” (FIG. 6, S203). In this specific example, the description in the “action execution path state” column of the processing target record is “State2”, and thus the process proceeds to step S206. In step S206, the state transition table generating unit 23 reads the processing target record. In this specific example, the state definition record in which the cell in the “action execution path state” column in the third row of the state definition record table is “State2” is read.

  Next, the state transition table generation unit 23 determines whether there is an event described in the “previous event” column in the processing target record (S207). In this specific example, since there is a description of the event “Start” in the “previous event” column in the third row of the state definition record table, the process proceeds to step S209.

  The state transition table generation unit 23 extracts a state definition record group having an action execution path state for the previous event from the state definition record table (S209 in FIG. 6). In this specific example, the state definition record in which the event “Start” is described in the “event” column in the state definition record table is extracted as an extracted record group, and the extracted record group is only the state definition record in the first row.

  Next, the state transition table generation unit 23 creates a row having an index that matches the action execution path state described in the “action execution path state” column of the extracted record group in the state transition table, and “event” of the processing target record. The action execution path state described in the “action execution path state” column of the processing target record is written in the state column of the processing target cell that is the intersection with the column having the index matching the event described in the “ In the action column of the processing target cell, the action described in the “action series” column of the processing target record is described (see S210). In this specific example, the extracted record group is only the first row of the state definition record table, and the action execution path state described in the “action execution path state” column of the first row is “State 0”. In addition, the event described in the “event” column of the processing target record is “E1 [False]”. Therefore, the processing target cell in the state transition table is determined to be a cell that is the intersection of the second row having “State 0” as an index and the third column from the left end having “E1 [False]” as an index. The state transition table generation unit 23 writes the action execution path state “State2” described in the “action execution path state” field of the processing target record in the state column (upper side of the cell) of the processing target cell. The state transition table generation unit 23 displays the action described in the “action series” column of the processing target record in the action column (lower side in the cell) of the processing target cell. However, since the processing target record “action series” column is blank, the action column of the processing target cell remains blank. (See S210). FIG. 12 shows an example of a state transition table in which “State2” is described in the processing target cell and the action column is left blank.

[State definition record table, 4th line]
Next, the state transition table generation unit 23 proceeds to step S205, and sets the next record in the state definition record table as a process target record (FIG. 6, S205). In this specific example, the state definition record in which the cell in the “action execution path state” column in the fourth row of the state definition record table of FIG. 5 is “State3” is determined as a new processing target record.

  Next, the state transition table generating unit 23 determines whether or not all the rows (records) of the acquired state definition record table have been read (see S203 in FIG. 6). In this specific example, the state transition table generation unit 23 determines that all rows have not been read (No in FIG. 6, S203).

  Next, the state transition table generation unit 23 determines whether the information described in the cell of the processing target record “action execution path state” is not “State0” (S203 in FIG. 6). In this specific example, since the description in the “action execution path state” column of the processing target record is “State3”, the process proceeds to step S206. In step S206, the state transition table generating unit 23 reads the processing target record. In this specific example, a state definition record in which the cell in the “action execution path state” column in the fourth row of the state definition record table is “State3” is read.

  Next, the state transition table generation unit 23 determines whether there is an event described in the “previous event” column in the processing target record (S207 in FIG. 6). In this specific example, since the events “E1 [True]” and “E1 [False]” are described in the “previous event” column in the fourth row of the state definition record table, the process proceeds to step S209.

  The state transition table generation unit 23 extracts a state definition record group having an action execution path state for the previous event from the state definition record table (see S209). In this specific example, the state definition record in which the events “E1 [True]” and “E1 [False]” are described in the “event” column in the state definition record table is extracted, and the extracted record is “E1 [True]”. Only the state definition record in the second row for “E1 [False]” is only the state definition record in the third row.

  Next, the state transition table generation unit 23 creates a row having an index that matches the action execution path state described in the “action execution path state” column of the extracted record group in the state transition table, and “event” of the processing target record. The action execution path state described in the “action execution path state” column of the processing target record is written in the state column of the processing target cell that is the intersection with the column having the index matching the event described in the “ In the action column of the processing target cell, the action described in the “action series” column of the processing target record is described (see S210 in FIG. 6).

  In the state definition record table, the extracted record group for “E1 [True]” is only the second row, and the action execution path state described in the “action execution path state” column of the second row is “State1”. is there. Further, the event described in the “event” column of the processing target record is “E2 [True]”. Therefore, the processing target cell in the state transition table is determined as a cell that is the intersection of the third row with “State1” as an index and the fourth column from the left end with “E2 [True]” as an index. The state transition table generation unit 23 writes the action execution path state “State3” described in the “action execution path state” field of the processing target record in the state column (upper side of the cell) of the processing target cell. Further, the state transition table generation unit 23 displays the action described in the “action series” column of the processing target record in the action column (lower side in the cell) of the processing target cell. However, since the action “A3” is described in the processing target record “action series” column, “A3” is described in the action column of the processing target cell. (See S210).

  Next, processing of the extracted record group for another event “E1 [False]” will be described. In the state definition record table, the extracted record for “E1 [False]” is only the third row, and the action execution path state described in the “action execution path state” column of the third row is “State2”. . Further, the event described in the “event” column of the processing target record is “E2 [True]”. Therefore, the processing target cell in the state transition table is determined as the cell that is the intersection of the fourth row with “State2” as an index and the left column with “E2 [True]” as an index. The state transition table generation unit 23 writes the action execution path state “State3” described in the “action execution path state” field of the processing target record in the state column (upper side of the cell) of the processing target cell. Further, the state transition table generation unit 23 displays the action described in the “action series” column of the processing target record in the action column (lower side in the cell) of the processing target cell. However, since no action is described in the “action series” column of the processing target record, nothing is written in the action column of the processing target cell. (See S210). FIG. 13 shows the state of the state definition record table and the state transition table at the time when the processing of the fourth row is completed.

[State definition record table, 5th line]
Next, the state transition table generation unit 23 proceeds to step S205, and sets the next record in the state definition record table as a process target record (FIG. 6, S205). In this specific example, the state definition record in which the cell in the “action execution path state” column in the fifth row of the state definition record table of FIG. 5 is “State 4” is determined as a new processing target record.

  Next, the state transition table generation unit 23 determines whether or not all rows (records) in the state definition record table have been read (see S203 in FIG. 6). In this specific example, the state transition table generation unit 23 determines that all rows have not been read (No in FIG. 6, S203).

  Next, the state transition table generation unit 23 determines whether or not the information described in the cell of the process target record “action execution path state” in the state definition record table is “State 0” (FIG. 6, S203). In this specific example, since the description in the “action execution path state” column of the processing target record is “State4”, the process proceeds to step S2066. In step S206, the state transition table generating unit 23 reads the processing target record. In this specific example, a state definition record in which the cell in the “action execution path state” column in the fifth row of the state definition record table is “State4” is read.

  Next, the state transition table generation unit 23 determines whether there is an event described in the “previous event” column in the processing target record (S207). In this specific example, since the events “E1 [True]” and “E1 [False]” are described in the “previous event” column in the fifth row of the state definition record table, the process proceeds to step S209 (FIG. 6). , S207, Yes).

  The state transition table generation unit 23 extracts a state definition record group having an action execution path state for the previous event from the state definition record table (see S209). In this specific example, in the state definition record table, the state definition records in which the events “E1 [True]” and “E1 [False]” are described in the “event” column are extracted, and “E1 [True]” is extracted. The record group is only the state definition record in the second row, and the extracted record group for “E1 [False]” is only the state definition record in the third row.

  Next, in the state transition table, the state transition table generating unit 23 includes a row having an index that matches the action execution path state described in the “action execution path state” column of the extracted record, and the “event” of the processing target record. Write the action execution path status described in the “Action execution path status” column of the processing target record in the status column of the processing target cell that is the intersection with the column having the index that matches the event described in the column. The action described in the “action series” column of the processing target record is described in the action column of the processing target cell (FIG. 6, S210).

  In the state definition record table, the extracted record group for “E1 [True]” is only the second row, and the action execution path state described in the “action execution path state” column of the second row is “State1”. is there. Further, the event described in the “event” column of the processing target record is “E2 [False]”. Therefore, the processing target cell in the state transition table is determined to be a cell that is the intersection of the third row with “State1” as an index and the left end with “E2 [False]” as an index from the fifth column. The state transition table generation unit 23 writes the action execution path state “State4” described in the “action execution path state” field of the processing target record in the state column (upper side of the cell) of the processing target cell. Further, the state transition table generation unit 23 displays the action described in the “action series” column of the processing target record in the action column (lower side in the cell) of the processing target cell. However, since nothing is described in the “action series” column of the processing target record, the action column of the processing target cell is left blank. (FIG. 6, S210).

Next, the processing of the extracted record for another event “E1 [False]” will be described. In the state definition record table, the extracted record group for “E1 [False]” is only the third row, and the action execution path state described in the “action execution path state” column of the third row is “State2”. is there. Further, the event described in the “event” column of the processing target record is “E2 [False]”. Therefore, the processing target cell in the state transition table is determined as a cell that is the intersection of the fourth row with “State2” as an index and the left column with “E2 [False]” as an index. The state transition table generation unit 23 writes the action execution path state “State4” described in the “action execution path state” field of the processing target record in the state column (upper side of the cell) of the processing target cell. Further, the state transition table generation unit 23 displays the action described in the “action series” column of the processing target record in the action column (lower side in the cell) of the processing target cell. However, since no action is described in the “action series” column of the processing target record, the action column of the processing target cell is left blank. (FIG. 6, S210).
FIG. 14 shows the state of the state definition record table and the state transition table at the time when the processing of the fifth row is completed.

[State definition record table, 6th line]
Next, the state transition table generation unit 23 proceeds to step S205, and sets the next record in the state definition record table as a process target record (FIG. 6, S205). In this specific example, the state definition record in which the cell in the “action execution path state” column is “State5” is determined as a new processing target record, which is the last row of the state definition record table of FIG.

  Next, the state transition table generation unit 23 determines whether or not all rows (records) in the state definition record table have been read (see S203 in FIG. 6). In this specific example, the state transition table generation unit 23 determines that all rows have not been read (No in FIG. 6, S203).

  Next, the state transition table generation unit 23 determines whether or not the information described in the cell of the process target record “action execution path state” in the state definition record table is “State0” (see S203 in FIG. 6). In this specific example, since the description in the “action execution path state” column of the processing target record is “State5”, the process proceeds to step S206. In step S206, the state transition table generating unit 23 reads the processing target record. In this specific example, the state definition record whose cell in the “action execution path state” column in the third row of the state definition record table is “State5” is read.

  Next, the state transition table generation unit 23 determines whether there is an event described in the “previous event” column in the processing target record (S207 in FIG. 6). In this specific example, since there are descriptions of events “E2 [True]” and “E2 [False]” in the “previous event” column in the sixth row of the state definition record table, the process proceeds to step S209 (FIG. 6). , S207, Yes).

  The state transition table generation unit 23 extracts a state definition record group having an action execution path state for the previous event from the state definition record table (S209 in FIG. 6). In this specific example, in the state definition record table, state definition records in which the events “E2 [True]” and “E2 [False]” are described in the “event” column are extracted, and the extracted record group is “E2 [True] "Is only the state definition record in the fourth row, and" E2 [False] "is only the state definition record in the fifth row.

  Next, the state transition table generation unit 23 includes a row having an index that matches the action execution path state described in the “action execution path state” column of the extracted record in the state transition table, and the “event” of the processing target record. Write the action execution path status described in the “Action execution path status” column of the processing target record in the status column of the processing target cell that is the intersection with the column having the index that matches the event described in the column. The action described in the “action series” column of the processing target record is described in the action column of the processing target cell (FIG. 6, S210).

  In the state definition record table, the extracted record group for “E2 [True]” is only the fourth row, and the action execution path state described in the “action execution path state” column of the fourth row is “State3”. is there. In addition, the event described in the “event” column of the processing target record is “End”. Therefore, the processing target cell in the state transition table is determined to be a cell that is the intersection of the fifth row with “State3” as an index and the left end with “End” as an index from the sixth column. The state transition table generation unit 23 writes the action execution path state “State5” described in the “action execution path state” column of the processing target record in the state column (upper side of the cell) of the processing target cell. Further, the state transition table generation unit 23 displays the action described in the “action series” column of the processing target record in the action column (lower side in the cell) of the processing target cell. However, since nothing is described in the “action series” column of the processing target record, the action column of the processing target cell is left blank. (FIG. 6, S210).

Next, the processing of the extracted record group for another event “E2 [False]” will be described. In the state definition record table, the extracted record group for “E2 [False]” is only the fifth row, and the action execution path state described in the “action execution path state” column of the fifth row is “State4”. is there. In addition, the event described in the “event” column of the processing target record is “End”. Therefore, the processing target cell in the state transition table is determined as the cell that is the intersection of the sixth row with “State4” as an index and the left column with “End” as an index. The state transition table generation unit 23 writes the action execution path state “State5” described in the “action execution path state” column of the processing target record in the state column (upper side of the cell) of the processing target cell. Further, the state transition table generation unit 23 displays the action described in the “action series” column of the processing target record in the action column (lower side in the cell) of the processing target cell. However, since no action is described in the “action series” column of the processing target record, the action column of the processing target cell is left blank. (FIG. 6, S210).
FIG. 15 shows the state of the state definition record table and the state transition table at the time when the process on the sixth line is completed.

[Blank processing]
Next, the state transition table generation unit 23 proceeds to step S205 and sets the processing target record as the next state definition record. However, since the state definition record table has no rows after the sixth row, it is determined that the last row has been reached. Next, the state transition table generation unit 23 proceeds to step S203, and determines whether or not the state definition record has ended (FIG. 6, S203). Here, the state transition table generating unit 23 determines that the state definition record has ended (FIG. 6, S203, Yes), and proceeds to step S211.

In step S211, the state transition table generating unit 23 describes “/” as information indicating that the corresponding field is blank in all blanks of the state transition table. FIG. 16 shows an example of a state transition table in which information indicating that the corresponding column is blank is described. The state shown in FIG. 16 is a completed state transition table.
Thus, the state transition table generation process is completed, and the state transition table shown in FIG. 16 is completed.

[Example 1]
Next, another example of this embodiment will be described. FIG. 17 is a diagram illustrating a flowchart that is an input / output order sequence specification input to the state transition table generation device according to the present embodiment. This flowchart is a flowchart showing the processing contents of the payment settlement system in the employee cafeteria.

When the state transition table generation device reads the flowchart of FIG. 17, it first executes state definition record table generation processing (see FIG. 3).
The flowchart of FIG. 17 includes 12 steps from step S301 to step S312. Among them, conditional branches are step S303, step S305, and step S308.

  The state transition table generating device, more specifically, the state definition record table generating unit, labels each process of the flowchart of FIG. 17, S301, S302, S304, S306, S307, S309, S310, S311, and S312 as an action, and A1 , A2, A4, A5, A6, A8, A9, A3, A7. In addition, the state transition table generation device, more specifically, the state definition record table generation unit, corresponds to True (corresponds to Yes branch) and False (corresponds to No branch) in each of the conditional branches S303, S305, and S308 in the flowchart of FIG. To E1 [True] (S303, Yes) and E1 [False] (S303, No), E2 [True] (S305, Yes), and E2 [False] (S305, No) ), E3 [True] (S308, Yes) and E3 [False] (S308, No).

  The state transition table generation device 11, more specifically the state definition record table generation unit 22, generates the state definition record table shown in FIG. 18 by continuing the state definition record table generation process (see FIG. 3). FIG. 18 is a diagram illustrating an example of the state definition record table generated from the flowchart of FIG. 17 by executing the state definition record table generation process.

  Upon receiving the state definition record table shown in FIG. 18, the state transition table generating device 11, more specifically the state transition table generating unit 23, executes state transition table generation processing (see FIG. 6) based on this, and the state transition table is generated. Is generated and output. FIG. 19 shows an example of the state transition table generated from the state definition record of FIG. 18 by the state transition table generation process.

[Example 1: Additional functions]
The state transition table generation device 11, more specifically, the event / action definition record generation unit 24, is a table in which the labels attached to the events and actions are associated with the contents of the events and actions. Action definition record "is generated.
FIG. 20 shows an example of an “event / action definition record” generated by the state transition table generation device, more specifically the state definition record table generation unit, when generating the state transition table from the flowchart shown in FIG. It is a figure.

  By generating and using such an “event / action definition record”, the user can more easily verify and examine the contents of the state transition table. For example, when the generated state transition table is displayed on the screen and the cursor or pointer is placed on a label (A1, etc.) in the state transition table, the “event / action definition record” is referenced, It is also possible to realize a function that opens a pop-up window and displays a “meaning” corresponding to the label therein.

[Example 2]
In the above-described example, the aspect in which the flowchart is used as the input / output order sequence specification that is the input of the state transition table generation device 11 has been described. For example, the source code of the program may be used. Hereinafter, an operation example of the state transition table generation device 11 when the source code of the program is handled as the input / output order series specification will be described.

First, the state transition table generating device 11 generates a state definition record table based on the source code. This is performed by executing the state definition record generation process shown in FIG. However, the if statement and the while statement are treated as “conditional branch”, and the other command statements are treated as “processing”.
The state transition table generation device 11 generates a state transition table based on the generated state definition record table. This process is performed by the state transition table generation process shown in FIG.

  FIG. 21 is a diagram illustrating an example of source code that is input to the state transition table generation device 11. FIG. 22 is a diagram showing a state where event and action labels are attached to the source code of FIG. FIG. 23 shows an example of the state definition record table obtained as a result of executing the state definition record table generation process (see FIG. 3) with the event and action labels attached as shown in FIG. FIG. 24 shows an example of the state transition table obtained as a result of executing the state transition table generation process (see FIG. 6) based on the state definition record table shown in FIG. That is, the state transition table generating device 11 can generate the state transition table shown in FIG. 24 from the source code shown in FIG.

[Summary]
According to this embodiment, it is possible to handle time-series input information such as a flowchart for a model checking support tool that automatically converts a check code using event-response type specifications such as a state transition table as input information. It becomes like this.
According to the present embodiment, even if the time series specification conditions and processing are appropriately converted to state transition events, conditions, and actions so as to be converted to a state transition system, the processing path according to the conditions Can be easy to understand.

[Second Embodiment]
Next, a second embodiment will be described. The second embodiment is different from the first embodiment in processing for labeling events and actions in conditional branches and processing. More specifically, the first embodiment defines a combination of an event and an action as an action execution path state, whereas the second embodiment differs in that an event is an action execution path. Yes.

[Example of device configuration]
FIG. 25 shows a configuration example of the state transition table generating device 11A according to the second embodiment. The state transition table generating device 11A is basically the same as the configuration of the state transition table generating device 11 according to the first embodiment, except that the state definition record generating unit 22A is replaced with the state definition record generating unit 22A. It is different in having. For the other components, the same components are denoted by the same reference numerals, and detailed description of these components is omitted.

[Example of operation]
Next, an operation example of the state transition table generation device 11A will be described. Since each of the input / output order sequence specification storage unit 21, the state transition table generation unit 23, and the event / action definition record generation unit 24 is the same as the operation in the first embodiment, description of these operations will be omitted. The operation of the state definition record generation unit 22A will be described below.

FIG. 26 and FIG. 27 are flowcharts showing an example of state definition record generation processing that is an operation of the state definition record generation unit 22A, and FIG. 27 is a flowchart following FIG.
The state definition record generation process, which is the operation of the state definition record generation unit 22A shown in FIGS. 26 and 27, is basically the same as the operation of the state definition record generation unit 22 shown in FIGS. 3A and 3B. The difference is in step S90A.

  In step S90A, the state definition record generating unit 22A creates two state definition records having the same state name (information for specifying the action execution path state), and sets “True” of the conditional branch as one of the records for the event. Register in the field and register "False" in the event field of the other record.

  The other steps are the same as the steps shown in FIGS. 3A and 3B according to the first embodiment. Therefore, the steps having the same processing contents are denoted by the same reference numerals, and detailed descriptions thereof are given. Is omitted.

  A state definition record is generated by the state definition record generation process in the second embodiment. A state transition table is generated from this state definition record by the same processing as the state transition table generation processing (see FIG. 6) of the first embodiment.

  The state transition table generated in the second embodiment can reduce the number of action execution path states (state definition records) compared to that in the second embodiment, and as a result is finally generated. It is also possible to generate a simplified state transition table and reduce the burden on the user when using the state transition table.

[Specific example 1]
A specific example of the operation example of the state transition table generation device 11A according to the second embodiment will be described. FIG. 28 is a flowchart (referred to as a “processing target flowchart”) that is the input / output order sequence specification 10 that is the basis of the state definition record table in this specific example. FIG. 28 is the same as the flowchart shown in FIG. 4 described above, and the description of the content of this flowchart is omitted. FIG. 29 is a diagram showing an example of a state definition record table generated from the process target flowchart of FIG.

  First, the state definition record table generation unit 22A assigns an event and an action number to each element of conditional branching and processing in the flowchart shown in FIG. 28 (S10 in FIG. 26). Specifically, an event number “E1” is assigned to the first conditional branch S101, and an event number “E2” is assigned to the second conditional branch S104. Action numbers “A1”, “A2”, and “A3” are assigned to actions S102, S103, and S104, respectively.

  Next, when the state definition record table generation unit 22 generates a state definition record table and reads “Start” which is the first element of the flowchart, it stores “State0” in the action execution path state column and the event. A record having the event name “Start” stored in the column is added to the state definition record table (FIG. 26, S20).

  Next, the state definition record table generation unit 22A determines whether all elements other than “End” have been read (S30 in FIG. 26). In this specific example, since not all elements have been read, the determination is “No” and the process proceeds to step S40.

  Next, after the determination in step S30, the state definition record table generation unit 22A reads the next element from the connected portion of the processing target flowchart (FIG. 26, S40). In this example, the element “E1” of the processing target flowchart is read.

  Next, the state definition record table generating unit 22 determines whether or not the read element is a conditional branch (S50 in FIG. 26). In this example, the element “E1” is determined to be a conditional branch (FIG. 26, S50, Yes).

  Next, the state definition record table generating unit 22A determines a state name that defines a state caused by the conditional branch (FIG. 26, S70). In this example, the state definition record table generation unit 22 defines the conditional branch “E1” as the state name “State1”.

  Next, the state definition record table generating unit 22A determines whether or not the conditional branch has been registered in the state definition record table as an event (S80 in FIG. 26). In this example, it is determined that the conditional branch “E1” is not yet registered in the state definition record table (FIG. 26, S80, No), and the process proceeds to step S90A.

  In step S90A, the state definition record table generating unit 22A creates two new state definition records in the state definition record table, registers the conditional branch “True” in the event field of one record, and records the other record. Register “False” of the conditional branch in the event column. In this example, the state definition record table generating unit 22A creates the second and third rows in the state definition record table of FIG. 29, and the state name “State1” in the “action execution path state” column of the second row. And “E1 [True]” in the “Event” column. Furthermore, the state definition record table generating unit 22 describes the state name “State1” in the “action execution path state” column of the third row and “E1 [False]” in the “event” column.

  Next, the state definition record table generating unit 22A registers the event of the record whose state is defined immediately before the two records in the event before the registered or registered event (FIG. 26, S100). In this example, the state definition record table generation unit 22A performs “previous event” corresponding to “E1 [True]” (second line) and “E1 [False]” (third line), which are the events registered immediately before. In the column, the event “Start” described in the “Event” column of the record (first line) in which the state has been defined immediately before is described.

Next, the state definition record table generating unit 22A returns to step S30 and then reads the element “A1” next to the element “E1” in step S40 (FIG. 26, S40).
Next, the state definition record table generating unit 22A determines whether or not the read element is a conditional branch. In this example, it is determined that the element “A1” is not a conditional branch (FIG. 26, S50, No).

  Next, the state definition record table generating unit 22A registers the element number of the read element in the state definition record table with the element (process) as an action for the event of the condition (S60 in FIG. 26). Specifically, “A1” is described in the “action series” column of the second row of the state definition record table shown in FIG.

  Next, the state definition record table generating unit 22A returns to step S30, and in the subsequent step S40, reads the element “A2” next to the element “A1” (FIG. 26, S40).

  Next, the state definition record table generating unit 22A determines whether or not the read element is a conditional branch (FIG. 26, S50). In this example, it is determined that the element “A2” is not a conditional branch (FIG. 26, S50, No).

  Next, the state definition record table generating unit 22A registers the element number of the read element in the state definition record table with the element (process) as an action for the event of the condition (S60 in FIG. 26). Specifically, “A2” is added and described in the “action series” column of the second row of the state definition record table shown in FIG.

  Next, the state definition record table generating unit 22A returns to step S30, and then reads the element “E2” next to the element “A2” in the processing target flowchart in step S40 (FIG. 26, S40).

  Next, the state definition record table generating unit 22A determines whether or not the read element is a conditional branch (FIG. 26, S50). In this example, the element “E2” is determined to be a conditional branch (FIG. 26, S50, Yes).

  Next, the state definition record table generating unit 22A determines a state name that defines a state caused by the conditional branch (FIG. 26, S70). In this example, the state definition record table generation unit 22A determines the conditional branch “E2” as the state name “State2”.

  Next, the state definition record table generating unit 22A determines whether or not the conditional branch has been registered in the state definition record table as an event (S80 in FIG. 26). In this example, it is determined that the conditional branch “E2” has not yet been registered in the state definition record table (FIG. 26, S80, No), and the process proceeds to step S90A.

  In step S90A, the state definition record table generating unit 22A adds two new state definition records to the state definition record table, registers “True” of the conditional branch in the event field of one record, and records the other record. Register “False” of the conditional branch in. In this example, the state definition record table generating unit 22 creates the fourth and fifth rows in the state definition record table shown in FIG. 29, and describes “State2” in the “action execution path state” column of the fourth row. And “E2 [True]” in the “Event” column. Furthermore, the state definition record table generating unit 22A describes “State2” in the “action execution path state” column of the fifth line and “E2 [False]” in the “event” column.

  Next, the state definition record table generation unit 22A registers the event of the record that defines the state immediately before the two records in the event before the registered or registered event (FIG. 26, S100). In this example, the state definition record table generation unit 22A has “E1 [True” described in the event column of the record (second and third line records) registered immediately before the registration of the fourth and fifth lines. ] ”(Second line) and“ E1 [False] ”(third line) are described in the“ previous event ”column of the fourth and fifth lines.

Next, the state definition record table generating unit 22A returns to step S30, and then reads the element “A3” next to the element “E2” in step S40 (FIG. 26, S40).
Next, the state definition record table generating unit 22A determines whether or not the read element is a conditional branch (FIG. 26, S50). In this example, it is determined that the element “A3” is not a conditional branch (FIG. 26, S50, No).

  Next, the state definition record table generating unit 22A registers the element number of the read element in the state definition record table with the element (process) as an action for the event of the condition (S60 in FIG. 26). Specifically, “A3” is described in the “action series” column in the fourth row of the state definition record table shown in FIG.

  Next, the state definition record table generating unit 22A returns to Step S30, and determines whether or not all elements other than the end (End) have been read (S30 in FIG. 26). In this example, the state definition record table generation unit 22A determines that all elements other than end (End) have been read (S30, Yes), and proceeds to step S110 in FIG.

  In step S110, the state definition record table generation unit 22A stores a state name including the current number of states in the action execution path state column and generates a new state definition record in which “End” is stored in the event column. It is added to the definition record table (FIG. 27, S110). In the example of FIG. 29, this corresponds to the record in the sixth row.

Next, the state definition record table generating unit 22A registers the event of the record that defines the state immediately before the two records in the event before the registered or registered event (S120 in FIG. 27). In this example, the state definition record table generation unit 22A has “E2 [True]” described in the event column of the record (records corresponding to the fourth and fifth lines) registered immediately before the sixth line registration. (Fourth line) and “E2 [False]” (Fifth line) are described in the “Previous event” column of the sixth line.
Thus, the state definition record table shown in FIG. 29 is completed based on the processing of the flowchart shown in FIG.

[Generate state transition table]
Next, the state transition table generation device 11A, more specifically, the state transition table generation unit 23 receives the data of the state definition record table shown in FIG. 29, and uses this data to generate a state transition table generation process (FIG. 6) to generate a state transition table. The contents of the state transition table generation process are the same as those in the first embodiment.
FIG. 30 shows an example of the state transition table generated from the data of the state definition record table shown in FIG.

[Example 2]
Another specific example of the operation example of the state transition table generating device 11A according to the second embodiment will be described. An example in which the state transition table is generated by using the state transition table generating device 11A in the IP address assignment processing shown in FIG.

  FIG. 31 is a sequence diagram illustrating an example of processing for assigning an IP address in a network including PC-1, PC-2, PC-3, and PC-4. Both PC-3 and PC-4 function as a DHCP server.

  First, the PC-1 determines whether or not there is an IP address at the time of activation, and if no IP address is assigned, it broadcasts a DISCOVER message to other devices in the network (S3101, S3102, and S3103).

  The PC-3 and PC-4, which are DHCP servers that have received the DISCOVER message, transmit an OFFER message that includes an IP address that is a candidate for allocation (S3104, S3105). In this example, it is assumed that PC-3 presents an IP address IP1, and PC-4 presents an IP address IP2.

  If there is no problem with the presented IP address, the PC-1 that is the client that has received the OFFER message from each of the PC-3 and PC-4 officially sends a REQUEST message requesting the IP to the server (S3106, S3107). In this example, it is assumed that PC-1 selects IP1 and transmits the REQUEST message.

  The PC-3 that has received the REQUEST message for IP1 confirms that it has been selected by returning the same user IP address. If there is no problem, it returns a “PACK” packet, and if there is a problem, “PNAK”. The packet is returned (S3108).

  The PC-1 that has received the PACK normally stores the user IP address specified by OFFER as its own IP address, and then internally configures communication using this IP address. On the other hand, when “PNAK” is returned, the DISCOVER is transmitted again (S3109).

  In this embodiment, among the processes shown in the above sequence diagram, the process flowchart of the PC-1 that is the client and the process flowchart of the PC-3 that is the DHCP server are prepared as the input / output order sequence specification 10, respectively. The state transition table generating device 11A generates a state transition table from each input / output order sequence specification 10.

[Client side]
FIG. 32 is a diagram illustrating an example of a process flowchart of the PC-1 that is a client. Data corresponding to this flowchart is input from the input / output order sequence specification 10 to the state transition table generation device 11A. FIG. 33 is a flowchart of FIG. 32 to which a state name (action execution path state) is attached. FIG. 34 is a diagram showing the state transition table generated by the state transition table generating device 11A from the flowchart of FIG. 32 (input / output order sequence specification 10) in the state transition diagram.

[DHCP server side]
FIG. 35 is a diagram illustrating an example of a processing flowchart of the PC-3 that is the DHCP server. Data corresponding to this flowchart is input from the input / output order sequence specification 10 to the state transition table generation device 11A. FIG. 36 is a flowchart of FIG. 35 to which a state name (action execution path state) is attached. State names (action execution path states) State1, State2, State3, and State4 are assigned to the branch conditions E1, E2, E3, and E4, respectively, and a record in the state definition record table is generated for each state name. FIG. 37 is a diagram showing a state transition table generated by the state transition table generating device 11A from the flowchart of FIG. 35 (input / output order sequence specification 10) in a state transition diagram.

  As a modification of the present embodiment, when conditional branches are continuous (FIG. 36, E2 to E3), this is handled as one conditional branch, and a state transition table is generated as one state. May be. When the above modification is applied to this example, conditional branches E2 to E4 are processed as one state “State 2”.

[Other]
As mentioned above, although embodiment of this invention was described, this invention is not limited to these, A various change, addition, a combination, etc. are possible in the range which does not deviate from the meaning of invention.
As a modification, the state transition table generation device 11 has both a state definition record generation unit 22 and a state definition record generation unit 22A, and selects one of them according to a user's specification to generate a state definition record table. It can also be modified to generate a state transition table based on it.

DESCRIPTION OF SYMBOLS 10 ... Input / output order series specification; 11 ... State transition table production | generation apparatus; 12 ... State transition table; 21 ... Input / output order series specification memory | storage part; 22, 22A ... State definition record generation 23: State transition table generation unit; 24 ... Event / action definition record generation unit

Claims (3)

Information specifying event and action is attached to conditional branching and processing in data representing input / output sequence specification, information specifying action execution path state is attached to one path without branch, and one action is executed A first generation means for generating a state definition record table, which has one record for a path state, and each record is information having an event, a previous event, and an action sequence;
Based on the state definition record table, there is one record for each action execution path state included in the state definition record table, and each record has a field corresponding to each event included in the state definition record table. A state transition table generation device comprising: a second generation unit that generates a state transition table that is information. Information specifying events and actions is attached to conditional branches and processes in data representing input / output sequence specifications, information specifying action execution path states is attached to conditional branches, and one action execution path state is added. A first generation means for generating a state definition record table which is information including an event, a previous event, and an action sequence;
Based on the state definition record table, there is one record for each action execution path state included in the state definition record table, and each record has a field corresponding to each event included in the state definition record table. A state transition table generation device comprising: a second generation unit that generates a state transition table that is information. The second generation unit extracts a state definition record group having an action execution path state with respect to a previous event in the processing target record of the state definition record table, and stores an event described in the previous event in the processing target record in an event column. This is the intersection of a row having an index that matches the action execution path status described in the action execution path status column of the state definition record and a column having an index that matches the event described in the event column of the processing target record. Write the action execution path status described in the action execution path status column of the processing target record in the status column of the processing target cell that is a cell, and if there is a description of the action in the action series column of the processing target record, enter that action. Write in the action column of the cell to be processed Mukoto, the state transition table generating apparatus according to claim 1 or 2 to generate a state transition table.

Images