权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

形式的仕様とプログラムの厳密なレビューの自動化についての研究

自动化正式规范和严格的程序审查的研究

基本信息

批准号：
15017280
负责人：
劉少英
金额：
$ 2.18万
依托单位：
Hosei University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research on Priority Areas
财政年份：
2003
资助国家：
日本
起止时间：
2003 至无数据
项目状态：
已结题

项目摘要

平成15年度には、ソフトウェアシステムの機能仕様及びプログラムの正確性を検証する厳密なレビュー技術を確立するために、以下の具体的な研究を行った。第一、検証すべき性質からレビュータスク木(review task tree)を自動生成するために必要なルール及びそのルールの正確性を確立した。基本的には、それらのルールが、一階述語論理を基く、レビューの分割統治法の原理を応用することによる形成されたものである。生成されたレビュータスク木は、検証すべき性質とその分品間の関係を示すだけでなく、レビュータスクの順番も定義する。従って、レビューする目標が明確になる。第二、レビューのプロセスを容易に成されるために、レビュータスク木とテスト技術を統合してレビュープロセスを支援する技術を開発した。この技術は、幾つかのテストケースを生成する基準を含め、様々な種類の論理式の真値を判断できる細かく基準も定義した。第三、レビュー・タスク木技術を支援するために、プロトタイプツールを開発した。このツールでは、論理式で表している形式的な性質から、その性質の正確性を検証するために必要なレビュータスク木を自動的及び手動的に生成することができる。生成されたタスク木の中のそれぞれのタスクの正確性を検証するときに、ツールによる、検証するタスクを決められ、そのタスクを容易にレビューすることができる。それぞれのタスクのレビュー結果により、ツールはトプレベールタスクの正確性を自動的に決めることができる。第四、プログラムの正確性の検証に関しては、「形式的仕様から要求された機能を抽出」、「プログラムからパスを抽出」、「機能とパスの対応関係を構築」、及び「機能に対して、各パスの正確性をレビューする」の四つのステップから構成されたレビュープロセスを定義し、各セデップのタスクを完成するために必要な詳細な技術を開発した。第五、プログラムを容易にレビューできるために、レビュープロセスの支援ツールを開発した。そのツールによる、プログラムから制御の流れ図(control flow diagram)を自動的に生成、図の中のそれぞれの文とプログラムの中の同じ文に自動的に連結、図から自動的にプログラムパスを生成、更に、各パスの正確性をレビューすることによる、プログラム全体の正確性に自動的に決めることができる。

In 2015, we conducted the following specific research on the functional description and legality of the software development system. First, the review task tree is automatically generated and the legitimacy of the case is established. The basic theory of the division of logic, the theory of the division of logic, the theory of the division of logic The relationship between the two products is shown in the table below. The purpose of the project is clear. Second, it is easy to develop the technology for the development of the Internet. This technology is based on the definition of the criteria for the generation of a logical expression, including the type of logical expression. Third, the development of wood technology The nature of the form, the legitimacy of the nature, and the necessity of automatic and manual generation of the logical expression. The legal nature of the product is verified by the user's permission. The result of the review is that it is necessary to make an automatic decision on the legality of the review Fourthly, the four categories of the legitimacy of the application are defined as follows: "the formal requirements are extracted from the function,""the application requirements are extracted,""the functional relationship is constructed," and "the functional requirements and the legitimacy of each application are determined." The technical details required for the completion of each project were developed. Fifth, the development of the support system for the project The control flow diagram is automatically generated, linked, updated, and determined for each legitimacy.