- 著者
- 森本 祥一 重松 真二郎 後藤 祐一 程 京徳
- 出版者
- 日本ソフトウェア科学会
- 雑誌
- コンピュータ ソフトウェア (ISSN:02896540)
- 巻号頁・発行日
- vol.23, no.3, pp.3_117-3_133, 2006 (Released:2006-09-01)
情報システムの設計・開発において,セキュリティ仕様とその検証は重要な課題となっている.検証を行うには基準が必要であるが,情報システムが備えるべきセキュリティの基準を定めることは難しい.このため本論文では,IT製品や情報システムのセキュリティ評価の国際標準であるISO/IEC15408を基準として採用し,これに基づいた情報セキュリティ仕様の形式手法による検証技法を提案する.本検証技法では,形式的に記述したISO/IEC15408のセキュリティ評価基準を用いて,対象となる情報システムの仕様がISO/IEC15408の基準を満たしているかどうかを定理証明とモデル検査により厳密に検証することができる.
1 0 0 0 プログラム依存グラフ可視化ツールの開発
ソフトウェアを開発,保守する際にはプログラムの振舞いを理解することが必要となる.プログラム中の各部分の理解を積み書ねて,プログラム全体としての動作を理解しなくてはならず手間や時間,そして経験や勘を要する作業となっている.これがプログラムの開発,保守を困難にしている大きな要因の1つだと考える.プログラムの理解を助けるための良い道具があれば,ソフトウェアの開発や保守の手間や時間を大幅に減少できる可能性がある.プログラム依存グラフはプログラムの理解を支援するのに有効だと考える.プログラム依存グラフとはプログラム中の文間に存在する依存関係を有向枝として表したグラフである.プログラム依存グラフは,デバッグ,プログラムの理解,保守,テスト,複雑さ評価などの幅広い応用が可能である.例えばデバッグなら,プログラム依存グラフを使うことでプログラムの中で誤りに関係する箇所だけを抽出し調べるといったことが可能になり,作業を効率化できる.さらにプログラム依存グラフを可視化することで,プログラム中の文間の関係が一目で分かり,プログラムの構造が理解しやすくなる.本研究ではプログラム依存グラフを可視化し,これをデバッグやプログラム理解などのソフトウェア開発の支援に応用する.