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

点击翻译按钮获取中文摘要

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