| 摘要 |
<p>In the present invention, when verifying software specifications, a formal model having a high automatic verification rate and to which refinements have been applied is generated from natural language input. This device, which assists in the verification of software specifications by converting software specifications delineated in a format containing natural language to a formal language delineation, has: a strategy editing means for editing a certification strategy for specifications configured from properties that are to be satisfied by the software specifications; a language conversion means that converts the configuring elements and properties of the specifications to a formal language component that is a configuring element of the formal language delineation; a skeleton generation means that, from the certification strategy and the formal language component, generates a formal language delineation skeleton that contains the configuring elements of a portion of the formal language delineation; and a formal language component disposition means that generates the formal language delineation by means of introducing the formal language component to the formal language delineation skeleton.</p> |
