|
複雑なソフトウェアシステムを数学的手法で厳密に検証する必要性が高まっている。そこで、ソフトウェアの形式モデルを複数の抽象度にわたって構築し、対象システムの構成要素を段階的に導入しつつモデルを検証する手法(段階的詳細化)が注目されている。このアプローチはモデルの保守・発展性の向上に貢献する可能性を秘めるが、その恩恵の大きさは導入される要素と導入の順序の選び方に大きく左右される。しかし、適切な要素やその導入順序を事前に選ぶことは難しい。
そこで本研究では、既存のモデルで導入されている要素や導入の順序を、モデルの整合性を保ちつつ自動で柔軟に変更する手法を構築する。さらに、提案手法を用いて様々な導入順に関して比較実験を行い、状況に応じた適切な導入順を選ぶための指針を確立する。これにより、既存のモデルで行われている詳細化を改良でき、形式モデルの保守・発展性を向上できるという点で本研究の意義は大きい。
平成30年度では特に下記の2つの問題に取り組んだ。第1に、公開されている多段階形式モデルを分析し、特に複数のモデルの要素間の関係について記述した式の形に着目して、パターンの定義を行った。これにより、モデルの保守・発展に効果的であることが経験的に知られているパターンを獲得した。第2に、詳細化の再構築手法を利用して、パターン由来の詳細化を含めてどのような詳細化をどのような順序で行うとモデリングと証明の複雑さの軽減に効果的であるかの分析を行った。
以上より、経験的に有効と知られている詳細化のパターンをもとに、図式を用いた直観的な指示で既存のモデルの保守・発展性を高める手法と、どのように詳細化を設計・改良すると有効かの指針を獲得した。
|
