モジュール間の整合性検査のための要求仕様記述の検証

概要

論文の詳細を見る
本論文では,応用ソフトウェアを構成する部分ソフトウェア(モジュール)の接続関係の妥当性を確証するための,要求仕様に対する全体的枠組みを考察する.この枠組みは,モジュール間の整合性の検証を考慮して構成された要求仕様記述形式および検証系からなる.本要求仕様記述は,各モジュールのインタフェースと挙動の定義およびその接続関係の定義から構成される.モジュールに対する手続き呼出しの時系列(トレース)により挙動が定義され,モジュール間での処理の移動条件により接続関係が定義される.本記述形式では,モジュールをデータ抽象化されたものとみなし,その仕様をブラックボックス的に記述できるために,モジュール内のデータ構造等の実現レベルの情報を考慮する必要がない.本記述の検証は,要求仕様記述を一階述語論理形式に変換し,処理が移動するときにモジュールの挙動が移動条件を満足することを反駁導出により求めることで実現されている.従来のソフトウェア検証法である不変表明法に比べ,本手法は,検証に用いる仕様として,モジュールのインタフェースと挙動およびモジュール間の接続関係を定義するだけでよく,記述対象が明確である点で仕様の記述が容易であり,より実際的であると考えられる.実験検証システムによる検証実験を通して,提案した記述形式の有効性を明らかにしている.
一般社団法人情報処理学会の論文
1990-01-15

モジュール間の整合性検査のための要求仕様記述の検証

スポンサーリンク

概要

著者

関連論文

スポンサーリンク