|
平成13年度には、形式的手法より実用性が高い形式工学手法SOFL(Structured Object-oriented Formal Language)に基づいて、形式的仕様とプログラムを検証するための必要な技術を以下の三つの研究を行った。第一、12年度まで研究して確立した厳密なfault treeレビュー技術と形式的仕様のテスト技術と組合せて、より強力な検証技術を研究した。この技術により、形式的仕様の整合性だけでなく、書いた仕様がユザーの機能要求に対して正しいかとうかも検証できる。形式的証明やプログラム分析や設計のレビュー技術などという伝統的な検証手法と比べて、今研究で提案した技術が検証する方法も違う、有効性もあることが明らかになった。仕様を検証するために、まず検証すべき条件を仕様から形式仕様記述言語の意味により導出し、それらの条件を基にレビューする目標を確立した上に、レビューの計画を図や表などで表現し、その計画に従ってテスト技術を利用しながら検証の目標をひとつずつレビューする。第二、ユザーの要求仕様を完全に正しく獲得するために、ソフトウェア開発する厳密的な詳細化(refinement)手法と仕様テスト技術を統合した手法を研究した。抽象的なユザー要求仕様書を厳密的な詳細化のルールにより段階的に発見し、それらの要求をS0FL言語で記述することによりユザー要求仕様書を完成することができる。伝統的な非形式的手法と比べて、形式的な詳細化は明確的なルールに従うことができるため、ソフトウェア支援ツールにより各段階の目標を指示することもでき、全ての要求を引き出す効果もあることが明らかになった。また、テスト技術を利用して各段階に獲得した仕様の正確性を検証することが出来る。第三、形式的仕様により実装されたプログラムをテストする技術を研究した。この技術によりプログラムは仕様書に対し正しいかとうかを検証することができる。テストを有効させるために、様々なテストケースの生成方法を設計し、それらの方法の効果を事例を通じて試して評価した。
|
