|
平成12年度は、ソフトウェア開発における形式的記述言語SOFLを用いて記述した形式的仕様を検証するために、厳密なレビュー(Rigorous Reviews)技術の研究を行った。厳密なレビューというのは、形式的証明を基に、仕様の様々な性質を確認するために検証することである。レビューに対しては、様々な技術が存在しているが、既存の技術ではほとんど非形式的仕様を対象としている。本年度の研究では、形式的仕様に適用する厳密なfault tree analysisという新しいレビュー技術を提案した。これは形式的証明とシステムの安全性を分析するfault tree analysisという技術を統合し、証明よりも高い実用性を持つ厳密なレビュー手法である。この技術では、形式的仕様の充足可能性(satisfability)、一致性(consistency)、完全性(completeness)、正確性(accuracy)及び予想されるシステムの安全性を分析するのに必要なタスクを木構造で表示、分析するプロセスを管理、そして分析によって発見された問題を報告することができる。この技術の一番重要な部分は仕様から木構造へ変換する必要なルールである。それのルールの正しさがレビューの効果に大きい影響を与える。SOFL仕様は一般にmoduleとCDFDの二つから構成されているので、その変換ルールとしてこれら二つの部分とともに考えることが必要である。さらに、この技術は他の実用的な検証技術、たとえば、仕様テスト、モデルチェッキング(model checking)等を統合して、より効果的な技術になると考えられる。
|
