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

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

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

長岡, 武志; 伊藤, 明彦; 岡野, 浩三他

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス, 2009, 109(170), 37-42

アクセス数:568件（2025-10-24 13:33 集計）

固定URL: https://hdl.handle.net/11094/27435

閲覧可能ファイル

ファイル	フォーマット	利用条件	サイズ	閲覧回数	利用開始日	説明	information
itr109_170_37	pdf	なし	765 KB	107	2014.04.11

論文情報

ファイル出力 EndNote Basic出力 Mendeley出力

タイトル	確率的モデル検査ツールを用いた実時間ネットワークシステムの検証手法の提案およびネットワークシミュレータ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　トノ　ヒカク
著者	著者名長岡, 武志 ; ナガオカ, タケシ ; Nagaoka, Takeshi
	NRID 1000060337053 1000060337053 著者名伊藤, 明彦 ; イトウ, アキヒコ ; Ito, Akihiko
	NRID 1000070252632 1000070252632 著者名岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
	NRID 1000030234438 1000030234438 researchmap permalink read0013799 read0013799 Scopus Author ID 7102741360 7102741360 著者名楠本, 真二 ; クスモト, シンジ ; 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
言語	日本語
ハンドルURL	https://hdl.handle.net/11094/27435
PISSN	09135685
NCID	AN10013287
アクセス権	open access
権利情報	Copyright © 2009 IEICE
権利情報	本文データはCiNiiから複製したものである
出版タイプ	Version of Record
カテゴリ	学術雑誌論文 Journal Article

資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
DCMI資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス. 2009, 109(170), p. 37-42
DC.title	確率的モデル検査ツールを用いた実時間ネットワークシステムの検証手法の提案およびネットワークシミュレータ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　トノ　ヒカク
DC.creator	長岡, 武志
	ナガオカ, タケシ
	Nagaoka, Takeshi
	伊藤, 明彦
	イトウ, アキヒコ
	Ito, Akihiko
	岡野, 浩三
	オカノ, コウゾウ
	Okano, Kozo
	楠本, 真二
	クスモト, シンジ
	Kusumoto, Shinji
DC.publisher	電子情報通信学会
	The Institute of Electronics, Information and Communication Engineers
	デンシ　ジョウホウ　ツウシン　ガッカイ
DC.language' scheme='DCTERMS.RFC1766	日本語
DC.type' scheme='DCTERMS.DCMIType	text
DCTERMS.issued' scheme='DCTERMS.W3CDTF	2009-07-30
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から複製したものである
DC.format	27435
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_public_url	https://hdl.handle.net/11094/27435

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

閲覧可能ファイル

論文情報

論文詳細を表示