確率的モデル検査ツールを用いた実時間ネットワークシステムの検証手法の提案およびネットワークシミュレータNS-2との比較

長岡, 武志; 伊藤, 明彦; 岡野, 浩三; 楠本, 真二

このアイテムのアクセス数:142件（2022-07-06 03:39 集計）

このアイテムへのリンクには次のURLをご利用ください:http://hdl.handle.net/11094/27435

閲覧可能ファイル

ファイル	フォーマット	サイズ	閲覧回数	説明
itr109_170_37	pdf	765 KB	54

論文情報

タイトル	確率的モデル検査ツールを用いた実時間ネットワークシステムの検証手法の提案およびネットワークシミュレータNS-2との比較
別タイトル	Verification for the Real-time Network Systems with the Probabilistic Model Checker and its Comparision with the Network Simulator NS-2
タイトル (ヨミ)	カクリツテキ　モデル　ケンサ　ツール　ヲ　モチイタ　ジツジカン　ネットワーク　システム　ノ　ケンショウ　シュホウ　ノ　テイアン　オヨビ　ネットワーク　シミュレータ　NS-2　トノ　ヒカク
著者	長岡, 武志長岡, 武志
	伊藤, 明彦伊藤, 明彦
	岡野, 浩三岡野, 浩三
	楠本, 真二楠本, 真二
著者の別表記	Ito, Akihiko
	Nagaoka, Takeshi
	Okano, Kozo
	Kusumoto, Shinji
著者 (ヨミ)	イトウ, アキヒコ
	ナガオカ, タケシ
	オカノ, コウゾウ
	クスモト, シンジ
キーワード等	実時間ネットワークシステム
	モデル検査
	PRISM
	シミュレーション
	形式的検証
	Real-time Network System
	Model Checking
	PRISM
	Simulation
	Formal Verification
抄録	実時間ネットワークシステムにおいてはネットワークで要求されるQoSを達成することが重要とされる.そこで,確率的振る舞いを持つシステムに対するモデル検査ツールPRISMに着目し,これを用いた実時間ネットワークシステムの詳細なモデル化方法,さらにそれらの結果を利用した形式的検証手法について述べる.また本稿では,提案手法の有用性を明らかにするために例題に適用し,ネットワークシミュレータNS-2によってモデル化に対するシミュレーション結果の比較,考察についても述べる.
抄録	For distributed systems, managing QoS parameters is a focal point of their quality. In this paper, focusing on PRISM, a model checking tool for probabilistic real-time systems, we present a new method to analysis real-time network systems detailed, and to implement formal verification with the use of this result. The paper also describes an application example and evaluation of the method with network simulator NS-2.
公開者	電子情報通信学会
公開者の別表記	The Institute of Electronics, Information and Communication Engineers
公開者 (ヨミ)	デンシ　ジョウホウ　ツウシン　ガッカイ
掲載誌名	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
巻	109
号	170
開始ページ	37
終了ページ	42
刊行年月	2009-07-30
ISSN	09135685
NCID	AN10013287
URL	http://hdl.handle.net/11094/27435
権利情報	Copyright © 2009 IEICE
権利情報	本文データはCiNiiから複製したものである
言語	日本語
カテゴリ	学術雑誌論文 Journal Article

著者版フラグ	publisher
NII資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
dcmi資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス.109(170) P.37-P.42
DC.title	確率的モデル検査ツールを用いた実時間ネットワークシステムの検証手法の提案およびネットワークシミュレータNS-2との比較
DCTERMS.alternative	Verification for the Real-time Network Systems with the Probabilistic Model Checker and its Comparision with the Network Simulator NS-2
DC.creator	長岡, 武志
	伊藤, 明彦
	岡野, 浩三
	楠本, 真二
DC.creator	Ito, Akihiko
	Nagaoka, Takeshi
	Okano, Kozo
	Kusumoto, Shinji
DC.publisher	電子情報通信学会
DC.language" scheme="DCTERMS.RFC1766	日本語
DCTERMS.issued" scheme="DCTERMS.W3CDTF	2009-07-30
DC.identifier" scheme="DCTERMS.URI	http://hdl.handle.net/11094/27435
DC.subject	実時間ネットワークシステム
	モデル検査
	PRISM
	シミュレーション
	形式的検証
	Real-time Network System
	Model Checking
	PRISM
	Simulation
	Formal Verification
DCTERMS.abstract	実時間ネットワークシステムにおいてはネットワークで要求されるQoSを達成することが重要とされる.そこで,確率的振る舞いを持つシステムに対するモデル検査ツールPRISMに着目し,これを用いた実時間ネットワークシステムの詳細なモデル化方法,さらにそれらの結果を利用した形式的検証手法について述べる.また本稿では,提案手法の有用性を明らかにするために例題に適用し,ネットワークシミュレータNS-2によってモデル化に対するシミュレーション結果の比較,考察についても述べる.
DCTERMS.abstract	For distributed systems, managing QoS parameters is a focal point of their quality. In this paper, focusing on PRISM, a model checking tool for probabilistic real-time systems, we present a new method to analysis real-time network systems detailed, and to implement formal verification with the use of this result. The paper also describes an application example and evaluation of the method with network simulator NS-2.
DC.rights	Copyright © 2009 IEICE
DC.rights	本文データはCiNiiから複製したものである
citation_title	確率的モデル検査ツールを用いた実時間ネットワークシステムの検証手法の提案およびネットワークシミュレータNS-2との比較
citation_author	長岡, 武志
	伊藤, 明彦
	岡野, 浩三
	楠本, 真二
citation_publisher	電子情報通信学会
citation_language	日本語
citation_date	2009-07-30
citation_journal_title	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
citation_volume	109
citation_issue	170
citation_firstpage	37
citation_lastpage	42
citation_issn	09135685
citation_public_url	http://hdl.handle.net/11094/27435
citation_keywords	実時間ネットワークシステム
	モデル検査
	PRISM
	シミュレーション
	形式的検証
	Real-time Network System
	Model Checking
	PRISM
	Simulation
	Formal Verification

閲覧可能ファイル

論文情報

論文詳細を表示