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

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

平成16年度には、ソフトウェアシステムの機能仕様とプログラムの整合性(consistency)と正当性(validity)を検証する厳密なレビュー技術の自動化方法の確立及びその方法を支援するツールの開発のために、以下の具体的な研究を行った。第一、検証すべき性質を形式的仕様から自動的に抜き出すアルゴリズムと支援ツールを開発した。第二、レビュータスク木と仕様テスト技術を統合してレビュープロセスを確立し、その技術を支援するツールを構築した。第三、プログラムは形式的設計仕様を満たすかどうかを検証するために、機能定義と実行パスの関係に基く仕様によるプログラムをレビューする方法を確立し、その方法の有効性を評価するために、銀行のATMシステムに応用することによりレビューの実験を行い、実験の結果を分析、その方法の有効性を確立した。第四、仕様によるプログラムをレビューする方法を高効率に支援するために、支援ツールを開発した。そのツールによりプログラムのレビューを行うには、仕様に定義された機能をプログラムで実装されたかどうかを検証だけでなく、定義されてないプログラムコードの正しさも検査できる。更に、以上の研究でソフトウェア検証の新たな課題も発見し、今後の研究を展開するには役に立つ材料を獲得した。