ソフトウェアの形成的仕様と設計の厳密な検証技術の研究

2000 Fiscal Year Annual Research Report

• Project/Area Number: 11680368
• Research Institution: Hosei University
• Principal Investigator: 劉 少英 法政大学, 情報科学部, 助教授 (90264960)
• Keywords: 形式的工学手法 / ソフトウェア検証 / 厳密なレビュー / 仕様分析 / 形式的仕様 / システム進化 / テスト / 形式的証明

Research Abstract

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

Research Products

• [Publications] Shaoying Liu: "Verifying Formal Specifications Using Fault Tree Analysis"Proceedings of International Symposium on Principle of Software Evolution, IEEE press. November. 272-281 (2000)
• [Publications] Shaoying Liu,Jim Woodcock: "Supporting Rigorous Reviews of Formal Specifications Using Fault Trees"Proceedings of Conference on Software Theory and Practice, IFIP 16^<th> World Computer Congress. August. 459-470 (2000)