文章基本信息
- 标题：事例研究：定理証明によるファイアウォールサーバモデルの検証
- 本地全文：下载
- 作者：矢竹 健朗 ; 片山 卓也
- 期刊名称：コンピュータ ソフトウェア
- 印刷版ISSN：0289-6540
- 出版年度：2009
- 卷号：26
- 期号：1
- 页码：1_111-1_126
- DOI：10.11309/jssst.26.1_111
- 出版社：Japan Society for Software Science and Technology
- 摘要：
本稿では，オブジェクト指向モデル検証ツールObjectLogicを用いて，ファイアウォールサーバのUMLモデルの検証を行った旨を報告する．ObjectLogicではメソッドが事前事後条件や不変表明を満たすことを定理証明器HOLで検証することが可能である．実験では，パケット処理を行うメソッドをシーケンス図により定義し，それがOCLにより定義された要求仕様を満たすことを検証した．本稿ではその有効性，問題点，改善法について考察する．
