WEKO3
アイテム
モジュール間の整合性検査のための要求仕様記述の検証
https://ipsj.ixsq.nii.ac.jp/records/15110
https://ipsj.ixsq.nii.ac.jp/records/15110f1dbac05-f4fd-4054-8bcb-fbc0c1c3edc4
名前 / ファイル | ライセンス | アクション |
---|---|---|
![]() |
Copyright (c) 1990 by the Information Processing Society of Japan
|
|
オープンアクセス |
Item type | Journal(1) | |||||||
---|---|---|---|---|---|---|---|---|
公開日 | 1990-01-15 | |||||||
タイトル | ||||||||
タイトル | モジュール間の整合性検査のための要求仕様記述の検証 | |||||||
タイトル | ||||||||
言語 | en | |||||||
タイトル | A Verification Method of Requirements Specification for Checking Consistency between Modules | |||||||
言語 | ||||||||
言語 | jpn | |||||||
キーワード | ||||||||
主題Scheme | Other | |||||||
主題 | 論文 | |||||||
資源タイプ | ||||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
資源タイプ | journal article | |||||||
その他タイトル | ||||||||
その他のタイトル | ソフトウェア工学 | |||||||
著者所属 | ||||||||
愛媛大学工学部情報工学科 | ||||||||
著者所属 | ||||||||
大阪大学工学部通信工学科/現在 (株)野村総合研究所 | ||||||||
著者所属 | ||||||||
神戸商船大学商船学部計測工学講座 | ||||||||
著者所属 | ||||||||
大阪大学工学部通信工学科 | ||||||||
著者所属 | ||||||||
愛媛大学工学部情報工学科 | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Department of Computer Science, Faculty of Engineering, Ehime University | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Department of Communication Engineering, Faculty of Engineering, Osaka University | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Faculty of Mercantile Marine, Kobe University of Mercantile Marine | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Department of Communication Engineering, Faculty of Engineering, Osaka University | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Department of Computer Science, Faculty of Engineering, Ehime University | ||||||||
著者名 |
山田, 宏之
× 山田, 宏之
|
|||||||
著者名(英) |
Hiroyuki, Yamada
× Hiroyuki, Yamada
|
|||||||
論文抄録 | ||||||||
内容記述タイプ | Other | |||||||
内容記述 | 本論文では 応用ソフトウェアを構成する部分ソフトウェア(モジュール)の接続関係の妥当性を確証するための 要求仕様に対する全体的枠組みを考察する.この枠組みは モジュール間の整合性の検証を考慮して構成された要求仕様記述形式および検証系からなる.本要求仕様記述は 各モジュールのインタフェースと挙動の定義およびその接続関係の定義から構成される.モジュールに対する手続き呼出しの時系列(トレース)により挙動が定義され モジュール間での処理の移動条件により接続関係が定義される.本記述形式では モジュールをデータ抽象化されたものとみなし その仕様をブラックボックス的に記述できるために モジュール内のデータ構造等の実現レベルの情報を考慮する必要がない.本記述の検証は 要求仕様記述を一階述語論理形式に変換し 処理が移動するときにモジュールの挙動が移動条件を満足することを反駁導出により求めることで実現されている.従来のソフトウェア検証法である不変表明法に比べ 本手法は 検証に用いる仕様として モジュールのインタフェースと挙動およびモジュール間の接続関係を定義するだけでよく 記述対象が明確である点で仕様の記述が容易であり より実際的であると考えられる.実験検証システムによる検証実験を通して 提案した記述形式の有効性を明らかにしている. | |||||||
書誌レコードID | ||||||||
収録物識別子タイプ | NCID | |||||||
収録物識別子 | AN00116647 | |||||||
書誌情報 |
情報処理学会論文誌 巻 31, 号 1, p. 136-143, 発行日 1990-01-15 |
|||||||
ISSN | ||||||||
収録物識別子タイプ | ISSN | |||||||
収録物識別子 | 1882-7764 |