JP6169302B2 - Specification configuration apparatus and method - Google Patents

Description

  The present invention relates to an apparatus and method for verifying system specifications in an initial process of system design and supporting the configuration.

  Conventionally, in the development of embedded systems and business systems, it is customary for designers who are familiar with the system to develop software. For this reason, even if there is ambiguity or error in the initial process of system design (hereinafter referred to as upstream process), it can be discovered and corrected in the later software development process, and it is carried over to the system operation stage after development. It was rarely found as a defect. However, as the system becomes more complex, it becomes difficult for the designer to grasp the entire system, and it is becoming impossible to remove defects by a method that relies on correction in the software development process.

  From such a background, it is considered that removing errors in the upstream process and reducing rework in the software development process are effective in improving the reliability and productivity of the software. In order to realize error elimination in the upstream process, it is important to check the consistency between the specification description of the upstream process and the specification, and the use of a specification description method suitable for the upstream process is progressing. The specification generally includes a description regarding data handled by the system, a description regarding processing executed by the system, and a description regarding dynamic behavior of the system. In the upstream process, a use case is used for a description relating to processing, and a processing flow diagram is used for a description relating to behavior, while a description relating to data is often abstracted and embedded in a use case.

  There is a relationship between the description of processing and the description of dynamic behavior in the specifications of the upstream process, and the system specifications are expressed as a whole of these. However, it is difficult to check the consistency of specifications across descriptions, and defects due to inconsistencies between descriptions cannot be completely removed. On the other hand, in Patent Document 1, specifications are described in four tables, a state transition table, an action table, a condition determination table, and a constraint condition table, and then combined to form a formal model. A method for verifying sex is disclosed.

  Specifically, the dynamic behavior is described in the state transition table, the process is described in the action table, the transition condition is described in the condition determination table, and the correspondence between the data described in the constraint condition table and the state is checked. The state transition table includes a state, an event, and a transition, a guard condition in which the transition occurs, and an action associated with the transition. The action table is composed of pre-conditions for causing an action, post-conditions to be established after the action, and processing contents representing element value update by the action. The condition determination table expresses a determination condition as to whether or not an action and a transition can be executed, and includes a guard condition and a precondition. The constraint table describes element values for each state.

  The apparatus of Patent Document 1 generates one formal model from the described specifications. This model is input to the model checker, and the consistency is verified using the model checker, thereby mechanically detecting the inconsistency of the described specification.

JP 2009-157661 A

  According to the specification description method described in Patent Document 1, when an event occurs when the system is in a certain state, the system executes a specified action for the state and the event, and transitions to the specified state. . Whether or not an action or transition can be executed is determined by the description in the condition determination table. This is considered to be suitable for describing the implementation specifications in the design process because it is easy to associate the call of the program module with the action.

  On the other hand, from the viewpoint of description of specifications of upstream processes, the classification of events and actions is complicated. While the specification description in the design process aims to clarify the implementation method in the computer, the specification description in the upstream process is intended to clarify the processing outline for people, and it is a specification that is easy for humans to grasp. It is required to be a description. For example, in the case described above, it is only necessary to be able to express concisely what happens and what effect is obtained as a result. In the method of Patent Document 1, since events are separated into events, and processing is separated into actions, it is necessary for a person to check the specifications and match the event name with the action name, and the action or transition can be executed. In order to determine whether or not, it is necessary to refer to the condition determination table. This makes it difficult for a person to grasp the specifications intuitively. When a formal model is generated from a specification that is difficult for humans to grasp and the consistency is verified, many inconsistencies in the specification are detected.

  Moreover, it aims at provision of the model creation assistance apparatus for inputting into a model checker, and it is premised on verifying using a model checker. Model checking is an exhaustive check for all combinations of state transitions, so it is an effective verification method for system specification verification that includes parallel operations. ineffective.

  Therefore, it is required that the consistency of specifications described by a person (designer) can be efficiently verified in the initial process of system design.

  The specification component device to be disclosed is a transition model input unit that inputs a transition model in which the dynamic behavior of the system is described by a combination of the system state and the state transition by the event, and the data value update accompanying the transition by the event is described A processing model input unit that inputs a processed model, a verification condition input unit that inputs a verification condition in which a condition of a data value that the system should satisfy is associated with a state, and a transition model and a processing model are associated with a common event A model combining unit that generates a combined model obtained by combining the transition model and the processing model, and a data flow analyzing unit that performs data flow analysis on the combined model and verifies that the verification condition is satisfied for the state.

  According to the disclosed specification component apparatus, it is possible to efficiently verify a specification written by a person in the initial process of system design.

It is a flowchart which shows the specification structure method in a specification structure apparatus. It is a figure which shows the structure of a specification structure apparatus. It is a figure which shows the example of a description of a transition model. It is a figure which shows the example of a description of a processing model. It is a figure which shows the example of description of verification conditions. It is a flowchart of the connection part of a model. It is a figure which shows the example of a connection model. It is a flowchart of a data flow analysis part. It is a flowchart which shows the procedure of the procedure 1 of a data flow analysis part. It is a flowchart which shows the procedure of the procedure 2 of a data flow analysis part. It is a flowchart which shows the procedure of the procedure 3 of a data flow analysis part. It is a flowchart which shows the procedure of the procedure 4 of a data flow analysis part. It is a figure which shows the example of the data value which a data flow analysis part produces | generates. It is a figure which shows the example of the data transition graph which a data flow analysis part produces | generates. It is a flowchart of a deadlock test | inspection model production | generation part. It is a flowchart which shows the procedure of the procedure A of a deadlock test model production | generation part. It is a flowchart which shows the procedure of the procedure B of a deadlock test model production | generation part. It is a flowchart which shows the procedure of the procedure C of a deadlock test model production | generation part. It is a flowchart which shows the procedure of the procedure D of a deadlock test model production | generation part. It is a figure which shows the example of the deadlock test | inspection model which a deadlock test | inspection model production | generation part produces | generates.

  The user inputs the transition model, processing model, and verification condition, and verifies that there is no inconsistency between the transition model and the processing model and that the verification condition that is input separately is satisfied using the specification component device. . In addition, when the transition model includes parallel operations related to a plurality of state transition sequences, the deadlock inspection model generated by the specification component device indicates that a deadlock in which the state transition does not proceed does not occur depending on the execution order of each state transition sequence. inspect.

  FIG. 1 is a flowchart showing a specification configuration method in the specification configuration apparatus. The user inputs a transition model (step 1), a processing model (step 2), and a verification condition (step 3) into the specification component device. These inputs may be performed in any order. The verification condition may be input after the next step 4.

  The specification component device collates the input transition model with the processing model, and generates a model in which both are combined (step 4). The specification configuration apparatus analyzes the data flow of the combined model, can execute the processing of the processing model in the order of the transition model, and further verifies that the verification condition is satisfied (step 5).

  The specification configuration apparatus determines that the verification condition is satisfied (step 6), and if the verification condition is not satisfied, the specification configuration apparatus proceeds to the inconsistent location output (step 7). If the verification condition is satisfied, the specification configuration apparatus determines whether or not there is a parallel operation (step 8). If there is no parallel operation, the input model is consistent, and the specification configuration apparatus ends the process.

  If the model includes a parallel operation, the specification configuration apparatus generates a deadlock inspection model for inspecting the presence or absence of deadlock (step 9). For example, SPIN model (Mordechai Ben-Ari, translated by Nakajima Earthquake, translated by Koichi Yatsu, Satoshi Nonaka, Taro Adachi: Introduction to SPIN Model Checking, Ohm Company 2010) The presence or absence of deadlock is inspected (step 10). The specification configuration apparatus determines whether or not there is a deadlock (step 11), and if there is a deadlock, executes the inconsistent location output (step 7). If there is no deadlock, the specification component apparatus determines that the input model is consistent and ends the process.

  FIG. 2 is a diagram showing the configuration of the specification configuration apparatus, which has components corresponding to the steps in FIG. The specification component device 21 outputs the verification result 27 and the deadlock inspection model 210.

  The transition model input unit 22 inputs a transition model from the user. FIG. 2 illustrates a mode in which the user operates the specification configuration device 21 and inputs a transition model. However, the present invention is not limited to this mode, and a mode in which a transition model described in advance by the user is input through a file or the like. But it ’s okay. Further, when a transition model is input, a form that supports user input with reference to a processing model and verification conditions may be used. The same applies to the processing model input unit 23 and the verification condition input unit 24.

  The processing model input unit 23 inputs a processing model from the user. The verification condition input unit 24 inputs verification conditions from the user.

  The model combining unit 25 generates a model obtained by combining the input transition model and the processing model. The data flow analysis unit 26 analyzes the data flow for the model generated by the model combining unit 25, can execute the processing model processing in the order of the transition model, and further verifies that the verification condition is satisfied. To do. The specification component device 21 outputs a verification result 27 by the data flow analysis unit 26.

  The deadlock check model generation unit 28 converts the model into a format that can be processed by the model checker for performing a deadlock check using a general model checker. The input of the deadlock inspection is not necessarily a verified model, and may be generated again from the transition model and the processing model.

  The specification component device 21 outputs the deadlock inspection model 29 generated by the deadlock inspection model generation unit 28. The user inputs the deadlock check model 29 to the model checker 210 and obtains the deadlock check result 211.

  FIG. 3 is a diagram illustrating a description example of the transition model input by the user. The transition model describes the flow of processing in a format that conforms to the processing flow used in the upstream process. SI represents a start state 31 and SE represents an end state 32. The flow of processing starts from the start state 31 and ends when the end state 32 is reached through a series of processes.

  Squares 32 to 36 indicate processing, and are called events here. An arrow represents a process to be executed next, and is referred to as a transition here. The circle connecting the arrows is called a state here.

  The processing flow represented by the transition model in FIG. 3 is as follows. The process starts from the start state 31, and after the processing of either the acceptance category determination new 32 or the acceptance category determination renewal 33 is executed, the contract creation 34 is executed. Thereafter, the contractor information registration 36 is executed to reach an end state 37, or the application category change 35 returns to either the acceptance category determination new 32 or the acceptance category determination renewal 33 again.

  A transition model can describe a plurality of such processing flows. That is, there can be a plurality of series of processes from the start state to the end state that do not intersect with each other. In that case, it is considered that those processing flows operate in parallel. Here, when a common event appears between different series of processing flows, the processing flow is considered to be synchronized through the common event.

  Such a plurality of descriptions is highly convenient because it can be described by dividing a large processing flow into a plurality of processing flows, but there is a possibility of deadlock depending on the execution order of the processing. The specification component device 21 checks in step 10 in FIG. 1 that no deadlock occurs when the transition model includes parallel operations.

  The description format of the transition model is not limited to the diagram format as shown in FIG. 3, and may be a text format or a table format as long as it can describe transitions according to states and events.

  FIG. 4 is a diagram illustrating a description example of the processing model input by the user. The processing model describes the data value condition for executing the process and the data value after the process in a format that conforms to the prior ex post description of the use case diagram used in the upstream process. Similar to the transition model, the process described in the process model is referred to as an event here. The event of the transition model and the event of the processing model must match, and the specification component device 21 checks when combining the models in step 4 of FIG.

  The processing of the acceptance category determination new 41 indicates that the value of the data acceptance category becomes new when the value of the data application category is new. Here, the description of the data value that is the premise of the processing is a condition part, processing The description of the data value set by is called a consequence.

  In the processing of the acceptance category determination renewal 42, values are set for two data in the consequent unit. This represents that the value of the data acceptance category is updated and the value of the data contract is confirmed.

  The process of creating the contracts 43a and 43b is an example in which one process is described by being divided into a plurality of items. The contract creation 43a indicates that the value of the contract is confirmed when the value of the data reception category is new, and the contract creation 43b indicates that nothing is performed when the value of the data reception category is renewal.

  The processing model of FIG. 4 further describes the processing of the reception category changes 44a and 44b and the processing of the contractor information registration 45.

  There may be a plurality of items described in the processing condition part, or zero. If the condition part is described as zero, it is considered that the condition always holds. In addition, when there are a plurality of description of the condition part, it is a premise of the processing that all these conditions are satisfied. A logical expression related to the data value may be described in the condition part.

  Similarly, the result part may include a plurality of items or zero. If there are a plurality of values, the values are set at the same time. If the number is zero, nothing is done as in the example of the contract creation 43b.

  The description format of the processing model is not limited to the table format as shown in FIG. 4, and any text format or data format can be used as long as the data value condition for the event to occur and the data value condition after the event can be described. It may be in diagram form.

  FIG. 5 is a diagram illustrating a description example of the verification condition input by the user. The verification condition is associated with the state of the transition model in FIG. 3 and lists data values expected when the process has progressed to that state.

  In FIG. 5, when the process represented by the transition model in FIG. 3 has advanced to the end state, that is, when a series of processes have been completed, it is requested that the value of the data contractor information is fixed (51). Similarly, when the process represented by the transition model in FIG. 3 proceeds to the end state, the application category value is new and the acceptance category value is new, or the application category value is updated and the acceptance category value is updated. (52) requesting that Like the latter, a logical expression may be described in the verification condition.

  The description format of the verification condition is not limited to the diagram format as shown in FIG. 5, and may be a text format or a table format as long as an expected data value can be described in association with the state.

  FIG. 6 is a flowchart of the model combining unit 25 (flow diagram showing the procedure for combining the transition model and the processing model in step 4 in FIG. 1). By this procedure, the input transition model and the processing model are collated and combined into one model.

  The model combining unit 25 extracts an event from the transition model (step 61), and extracts an event from the processing model (step 62). The model combining unit 25 determines whether or not these events match (step 63), and if they do not match, outputs that they do not match (step 67) and ends.

  If the event of the transition model matches the event of the processing model, the model combining unit 25 extracts a state from the transition model (step 64), and constructs a directed graph having the state as a node and the event as an edge (step 65). ). The model combining unit 25 adds nodes corresponding to the start state and the end state to the configured directed graph and connects them with edges (step 66).

  A model configured by combining the transition model and the processing model in this manner is referred to as a combined model here. Since a transition model can generally include a plurality of processing flows, a single coupled model can have a plurality of directed graphs.

  FIG. 7 is a diagram illustrating an example of a combined model. This example corresponds to the transition model of FIG. 3 and the processing model of FIG. 4, and the combined model is composed of one directed graph. In FIG. 7, a circle represents a directed graph node, and an arrow represents an edge. The label (name) of the edge is an event name.

  FIG. 8 is a flow diagram of the data flow analysis unit 26 (flow diagram showing the procedure of data flow analysis in step 5 of FIG. 1). The data flow analysis unit 26 adds data and a change in its value on the directed graph obtained by combining the transition model and the processing model. At this time, since a plurality of sets of data values generally correspond to a state of being a node of a directed graph, the data flow analysis unit 26 provides a method for processing them. Also, as shown in FIG. 7, a directed graph generally includes branching, merging, and repetition, so a method for preventing repeated processing of a set of processed data values is also provided.

  The data flow analysis unit 26 allocates a storage area D for storing a plurality of sets of data values to all nodes of the directed graph (step 81). The assigned initial value of D is empty. The data flow analysis unit 26 stores the set of initial data values in the storage area D of the node corresponding to the start state (step 82).

  In general, there are a plurality of sets of initial data values, and for each of them, the data flow analysis unit 26 analyzes changes in data values when the processing models are executed in the order of transition models. The data flow analysis unit 26 executes this analysis by calling the procedure 1 (step 83).

  When step 83 ends, a data value set is added to each node, so the data flow analysis unit 26 verifies that these satisfy the verification condition. For this verification, the data flow analysis unit 26 obtains a set of all data values in the storage area D specified in the verification condition (step 84), and determines whether it satisfies the verification condition (step 85). ).

  If the verification condition is not satisfied, the data flow analysis unit 26 outputs a malfunction (step 86) and ends. If the verification condition is satisfied, the data flow analysis unit 26 ends, assuming that the transition model matches the processing model.

  FIG. 9 is a flowchart showing the procedure of the procedure 1 of the data flow analysis unit 26. The procedure 1 calls the procedure 2 for executing the data flow analysis for all initial data sets (step 91).

  The procedure 1 sets a node n processed by the procedure 2 and a data value set d to be processed to an initial data set. Specifically, n is set as a start node (step 92), d is set as a set of initial data (step 93), and procedure 2 is called (step 94).

  FIG. 10 is a flowchart showing the procedure 2 of the data flow analysis 26. In the procedure 2, for a given node n and data value set d, a data value set in a destination node that is transitioned by an event is calculated for all events that can occur in n.

  Therefore, the procedure 2 obtains an outward edge from the node n (step 101). If there is an outward edge (step 102), all the outward edges from n are sequentially executed (step 103), and the procedure 3 is called with the edge to be processed as e (step 104) (step 105).

  In step 102, when there is no outward edge from n, it means that there is no transition destination from n, so procedure 2 determines whether n is in an end state (step 106), and the end state If it is, the process ends, and if it is not in the end state, it outputs that the transition model is inconsistent (step 107).

  FIG. 11 is a flowchart showing the procedure of the procedure 3 of the data flow analysis 26. The procedure 3 refers to the processing model for a given edge e and data value set d, selects e that can occur under d, and calculates the data value after the transition.

  In general, since there are a plurality of processing model items for the same event, a plurality of transition destinations may exist for a given edge e and data value set d. Procedure 3 calculates a set of data values for all these transition destinations.

  Therefore, the procedure 3 selects an item whose condition part of the process model item matches d from the event corresponding to e (step 111). If such items exist (step 112), procedure 3 calls procedure 4 for all of those items (step 113) (step 114).

  On the other hand, if there is no processing model item whose condition part matches d, it means that the processing cannot proceed according to the processing flow of the transition model. Is output (step 115).

  FIG. 12 is a flowchart showing the procedure of the procedure 4 of the data flow analysis unit 26. The procedure 4 calculates a pair of data values of the transition destination from the given data value pair d, the node n, and the edge e, adds the data value pair to the storage area D of the transition destination node, and advances the node to the transition destination node. Thus, the procedure 2 of the data flow analysis unit 26 is recursively called.

  Specifically, the procedure 4 calculates a set dn + 1 of the data value of the transition destination from the result part and d of the item of the processing model selected in the procedure 3 (step 121). The procedure 4 follows the edge e to obtain the transition destination node n + 1 (step 122), and obtains a data value storage area Dn + 1 associated with the node n + 1 (step 123).

  Procedure 4 determines whether a data value set dn + 1 exists in Dn + 1 (step 124). If not, dn + 1 is added to Dn + 1, and an edge is moved from dn to dn + 1. (Step 125). Since one of the processes related to the change of the data value set dn by the edge e is completed from the node n, the node is advanced by one, and the procedure 2 is called with n + 1 as n and d + 1 as d (step 126).

  On the other hand, if dn + 1 exists in Dn + 1 at step 124, it means that the analysis on the data value set dn + 1 has already been completed at node n + 1. An edge from to dn + 1 is stretched (step 127), and the process ends.

  In FIG. 12, in order to record how the set of data values has changed, in step 125 and step 127, procedure 4 has an edge from dn to dn + 1. As a result, a directed graph with a set of data values as a node and an event as an edge is formed separately from the directed graph with a state as a node and an event as an edge. Hereinafter, this is referred to as a data transition graph. A data transition graph facilitates tracking changes in a set of data values and improves verification efficiency during deadlock verification.

  FIG. 13 is a diagram illustrating an example of a set of data values generated by the data flow analysis unit 26. This figure corresponds to the example of the transition model of FIG. 3 and the processing model of FIG.

  The balloon in FIG. 13 represents the storage area D associated with each node. A set of codes surrounded by <and> in D represents a set of data values in that state, and in the figure, the order is <application category, acceptance category, contract, contractor information>. -Indicates that the value has not been determined.

  A balloon 131 indicates that two initial data sets <new,-,-,-> and <update,-,-,-> exist in the start state. This is because there are a set of data values whose data values are not determined except that the application category is new in the starting state, and a set of data values whose data values are not determined except that the application category is update. Represents what to do.

  A balloon 132 indicates a set of data values in the next state after the start state. In addition to the data value pairs from the starting state, there are four data value pairs because there are data value pairs returned by the event application category change. A balloon 135 is a set of data values after event contractor information registration, and a balloon 136 is a set of data values in the end state.

  In the example of the verification condition in FIG. 5, the contractor information is confirmed in the final state (51), the application category is new and the reception category is new, or the application category is renewal and the reception category is also renewal. (52) is requested, and it can be easily verified that the balloon 136 satisfies this condition. This verification is performed at step 84 and step 85 in FIG.

  FIG. 14 is a diagram illustrating an example of a data transition graph generated by the data flow analysis unit 26. A set of two initial data values of the balloon 131 in FIG. 13 corresponds to the node 141 and the node 142 in FIG. Similarly, balloon 132 corresponds to node 143 to node 146, balloon 133 corresponds to node 147 to node 149, balloon 134 corresponds to node 1410 to node 1411, balloon 135 corresponds to node 1412 to node 1413, and balloon 136 corresponds to node 1414 to node 1415. .

  FIG. 14 shows the result of extending the edge from dn to dn + 1 in steps 125 and 127 of FIG. As a result, a data transition graph is constructed in which a set of data values is a node and an event is an edge. The data transition graph records how the set of data values has changed, and is stored in the memory of the specification component device 21 for use by the deadlock check model generation unit 28.

  FIG. 15 is a flowchart of the deadlock check model generation unit 28 (flow chart showing a procedure for generating a deadlock check model in step 9 of FIG. 1). When the transition model includes parallel operations, that is, when there are a plurality of independent processing flows in the transition model, the specification configuration device 21 uses the model checker 210 to check whether there is a deadlock between them. To do. FIG. 15 shows a procedure for generating a deadlock check model 29 that is input to the model checker 210.

  The deadlock checking model 29 includes a description of a process corresponding to the combined model generated from each processing flow, a description of a cooperative process that synchronizes between them, and a description of shared information between processes. Therefore, the deadlock check model generation unit 28 calls the procedure A to generate inter-process shared information (step 151), and then calls the procedure B to generate a linked process description (step 152). Thereafter, for all connection models (step 153), the procedure C is called to generate a process description (step 154).

  FIG. 16 is a flowchart showing the procedure of the procedure A of the deadlock inspection model generation unit 28. The procedure A generates a description of an event passing channel and a state variable shared between processes. Therefore, the procedure A generates a channel for passing the event (step 162) and generates a state variable (step 163) for all connection models (step 161). In addition, the data node of the data transition graph is numbered and set as the value of the state variable (step 164).

  FIG. 17 is a flowchart showing the procedure B of the deadlock check model generation unit 28. The procedure B generates a description of the cooperation process. The cooperation process generates an event that can occur under the information of the data transition graph of each connection model, and transmits the event to the process generated from each connection model through the channel.

  The procedure B generates a process framework (step 171), and executes steps 173 to 174 for all events e (step 172). That is, for all the data transition graphs, a data node having e as an outward edge is extracted (step 173), and when the value of the state variable is the extracted data node in all connection models related to e, the event e is set. A sentence to be generated is generated (step 174). A statement for transmitting the generated event to each process through the channel is generated (step 175).

  FIG. 18 is a flowchart showing the procedure of the procedure C of the deadlock inspection model generation unit 28. Procedure C generates a process description for each combined model that operates in parallel.

  The procedure C generates a sentence for receiving an event through the channel (step 181). The procedure C generates a statement that assigns the start data node of the data transition model to the state variable corresponding to the initial state (step 182), and the value of the state variable corresponding to the end state ends the data transition model A sentence that is a data node is generated (step 183). When there are a plurality of initial values, there are a plurality of start data nodes of the data transition model. However, since a process description is generated for the combined model, a dummy start node that transitions to these start data nodes is set to 1 Set one.

  The procedure C calls the procedure D for all the data nodes except the start data node and the end data node in order to generate a description about the data node in the intermediate state between the initial state and the end state (step 184).

  FIG. 19 is a flowchart showing the procedure of the procedure D of the deadlock inspection model generation unit 28. Procedure D describes a transition due to an event based on the data transition graph.

  The procedure D extracts an outward edge and a transition destination node from the data nodes of the data transition graph (step 191). The procedure D generates a statement for replacing the state variable with the transition destination node when the value of the state variable is a data node having an outward edge and the event is an outward edge (step 192). The procedure D assigns a name to the data node of the data transition graph and sets it as the value of the state variable (step 193).

  FIG. 20 is a diagram illustrating an example of the deadlock inspection model 29 generated by the deadlock inspection model generation unit 28. The deadlock inspection model 201 is output in such a text format, for example. The deadlock checking model 201 includes a description (202) of information shared between processes, a description (203) of a cooperation process, and a description (204a, 204b) of a process corresponding to each combined model.

  A description (202) of information shared between processes is generated by the procedure A (FIG. 16) of the deadlock check model generation unit. In this example, channels cA and cB and state variables stateA and stateB are created for combined models A and B.

  The description (203) of the cooperation process is generated by the procedure B (FIG. 17) of the deadlock inspection model generation unit 28. In this example, when A is a1 and B is b1, the shared event e1 is transmitted through the channel. On the other hand, when A is in a2, event e2 is transmitted through the channel regardless of B. e2 is an event related to the transition of A, not a shared event.

  The process descriptions (204a, 204b) are generated by the procedure C (FIG. 18) and the procedure D (FIG. 19) of the deadlock check model generation unit 28. Each process first sets a state variable to an initial state. Thereafter, an event is received through the channel, a transition destination state is determined from the value of the current state variable and the received event, and is assigned to the state variable.

  In the deadlock checking model 29, a deadlock occurs when a process waits for the occurrence of a shared event, while the corresponding process waits for the occurrence of another shared event or terminates the event occurrence. The deadlock checking model 29 configured in this way is input to the model checker 210, and the presence or absence of deadlock is checked.

  According to the specification configuration apparatus of the present embodiment, it is possible to efficiently verify a specification written by a person in the initial process of system design.

  In addition, upstream designers can write specifications in a way that corresponds to the processing flow and use cases, and verify the consistency between them, so in the fields of embedded systems and business systems, the upstream design of complex systems Can be performed with high reliability and efficiency.

  21: Specification component device 22: Transition model input unit 23: Processing model input unit 24: Verification condition input unit 25: Model combination unit 26: Data flow analysis unit 27: Verification result 28: Deadlock check Model generation unit, 29: deadlock inspection model, 210: model checker, 211 verification result.

Claims (12)

A transition model input unit for inputting a transition model in which the dynamic behavior of the system is described by a combination of the state transition of the system and the state transition by an event;
A processing model input unit for inputting a processing model describing an update of a data value accompanying the transition by the event;
A verification condition input unit for inputting a verification condition in which the condition of the data value to be satisfied by the system is described in association with the state;
A model combining unit that generates a combined model obtained by combining the transition model and the processing model by associating the transition model and the processing model with the common event; and
A specification configuration apparatus comprising: a data flow analysis unit that performs data flow analysis on the combined model and verifies that the verification condition is satisfied for the state. When the event of the transition model and the event of the processing model match, the model combining unit configures a directed graph with the state extracted from the transition model as a node and the event as an edge, and a start state The specification composition device according to claim 1, wherein a new node corresponding to an end state is added, and the combined model is generated by connecting the directed graph and the new node with a new edge. Wherein the data flow analysis unit, on the directed graph, based on the updating of the data values described in the process model, by adding the data value, the data value obtained by adding the condition of the data values The specification composition device according to claim 2, wherein it is verified that it is satisfied. The deadlock check model generation unit that generates a deadlock check model for performing a deadlock check using a model check method when the transition model includes parallel operations. Specifications configuration equipment. 5. The deadlock checking model includes a description of a process corresponding to the coupling model, a description of a cooperative process that synchronizes between the processes, and a description of shared information between the processes. The specification component device described in 1. The specification configuration according to claim 4, wherein information regarding a change in the data value based on the update of the data value described in the processing model by the data flow analysis unit is used in the deadlock check. apparatus. A specification configuration method using a specification configuration device, wherein the specification configuration device is:
Input a transition model that describes the dynamic behavior of the system by combining the state transition of the system and the state transition caused by an event.
Input a processing model describing the update of the data value accompanying the transition by the event,
Enter a verification condition describing the condition of the data value that the system should satisfy in association with the state,
By associating the transition model and the processing model with the common event, a combined model that combines the transition model and the processing model is generated,
A specification configuration method characterized by performing data flow analysis on the combined model and verifying that the verification condition is satisfied for the state. When the event of the transition model and the event of the processing model match, the specification configuration device configures a directed graph with the state extracted from the transition model as a node and the event as an edge, and a start state, 8. The specification composition method according to claim 7, wherein a new node corresponding to an end state is added, and the combined model is generated by connecting the directed graph and the new node with a new edge. The specification component devices, on the directed graph, based on the updating of the data values described in the process model, by adding a pre-Symbol data values, before the addition Symbol data value condition of the data values 9. The specification composition method according to claim 8, wherein it is verified that the condition is satisfied. The specification configuration apparatus according to claim 7, wherein the specification configuration device generates a deadlock check model for performing a deadlock check using a model check method when the transition model includes a parallel operation. Method. 11. The deadlock checking model includes a description of a process corresponding to the coupling model, a description of a cooperative process that synchronizes between the processes, and a description of shared information between the processes. Specification configuration method described in 1. 11. The specification configuration method according to claim 10, wherein the specification configuration apparatus uses information regarding a change in the data value based on the update of the data value described in the processing model in the deadlock check. .

Images