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

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

本年度には、最新のソフトウェアレビューあるいは検査の手法について全面的に調べたうえで、三つの問題点に集中して研究を行った。第一、形式的仕様の整合性を検証するために必要な性質(例えば、内部一致性、不変数とプロセスの一致性、充足性、及び統合一致性など)を定義し、親和性良い「レビュー木」、という言語を設計し、性質とレビュー木を基に厳密な仕様レビュー手法を開発した。この手法では、仕様の整合性をレビューするために、まず検証すべき性質を仕様要素から自動的に生成及び論理式で表示する。次は、生成された論理式からレビュー木へ自動的に変換する。その後、レビュー木により、基本的な論理部品をレビューする。最後は、レビューの結果を評価し、仕様にエラーがあるかどうかを判断する。第二、形式的仕様レビューの手段の一つとしての「仕様シミュレーション」技術を提案した。この技術を用いて、形式的仕様の各部品(例えば、プロセス、モジュール、クラス、CDFDなど)を動的にレビューすることができる。例えば、プロセスをシミュレーションするために、まず入力と出力変数に具体的な値を生成して、次はそれらの値を用いてプロセスを評価する。その結果により、プロセス仕様にエラーがあるかどうかを判断する。第三、仕様要素を統合してシステムの構造を反映するCDFDの正確性を厳密な分析するために必要な論理システムを設計した。この論理システムと前述した厳密なレビュー手法を統合することにより、実用的な分析技術の開発ができると考える。