確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について

長井, 栄吾; 岡野, 浩三; 楠本, 真二

確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について

長井, 栄吾; 岡野, 浩三; 楠本, 真二

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス, 2006, 105(597), 19-24

アクセス数:473件（2025-07-03 22:54 集計）

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

閲覧可能ファイル

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

論文情報

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

タイトル	確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について
	A Verification Considering the Network Delay for Real-time Distributed Systems with the Probabilistic Model Checker PRISM
	カクリツテキ　モデル　ケンサ　ツール　PRISM　ニ　ヨル　リアルタイム　ブンサン　システム　ノ　ネットワーク　チエン　ヲ　コウリョ　シタ　ケンショウ　シュホウ　ニ　ツイテ
著者	著者名長井, 栄吾 ; ナガイ, エイゴ ; Nagai, Eigo
	NRID 1000070252632 1000070252632 著者名岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
	NRID 1000030234438 1000030234438 researchmap permalink read0013799 read0013799 Scopus Author ID 7102741360 7102741360 著者名楠本, 真二 ; クスモト, シンジ ; Kusumoto, Shinji
キーワード等	リアルタイム分散システム
	モデル検査
	PRISM
	形式的検証
	Real-time Distributed System
	Model Checking
	Formal Verification
抄録	モデル検査など形式モデルに基づくソフトウェアシステムの形式的検証は高い信頼性を持つソフトウェアの構築を可能にすると期待されている.さらに,分散システムにおいてはネットワーク上の遅延,遅延変動(ジッタ),帯域幅,パケットロスパラメータなどを管理して,要求されるQoSを達成することが重要とされる.そこで,本研究では確率的振る舞いを持つシステムに対するモデル検査ツールPRISMに着目し,これを用いたリアルタイムマルチメディアシステムのネットワーク遅延を考慮した形式的検証手法を提案する.また本論文では,提案手法の有用性を明らかにするために例題に適用し,その評価と考察についても述べる.
抄録	Formal verification techniques, especially model checking techniques are promising techniques in software developing due to their ability of exhaustive checking. For distributed systems, managing QoS parameters, such as latency, network delay, jitters, bandwidth and packet loss, is a focal point of their quality. In this paper, focusing using PRISM, a model checker for probabilistic real-time systems, we present a new method to analysis real-time multi-media systems considering network properties. The paper also describes an application example and the result.
出版者	電子情報通信学会
	The Institute of Electronics, Information and Communication Engineers
	デンシ　ジョウホウ　ツウシン　ガッカイ
収録物名	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
巻(号)	105(597)
ページ	19-24
刊行年月	2006-01-27
言語	日本語
ハンドルURL	https://hdl.handle.net/11094/27429
PISSN	09135685
NCID	AN10013287
アクセス権	open access
権利情報	Copyright © 2006 IEICE
権利情報	本文データはCiNiiから複製したものである
出版タイプ	Version of Record
カテゴリ	学術雑誌論文 Journal Article

資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
DCMI資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス. 2006, 105(597), p. 19-24
DC.title	確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について
	A Verification Considering the Network Delay for Real-time Distributed Systems with the Probabilistic Model Checker PRISM
	カクリツテキ　モデル　ケンサ　ツール　PRISM　ニ　ヨル　リアルタイム　ブンサン　システム　ノ　ネットワーク　チエン　ヲ　コウリョ　シタ　ケンショウ　シュホウ　ニ　ツイテ
DC.creator	長井, 栄吾
	ナガイ, エイゴ
	Nagai, Eigo
	岡野, 浩三
	オカノ, コウゾウ
	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	2006-01-27
DC.subject	リアルタイム分散システム
	モデル検査
	PRISM
	形式的検証
	Real-time Distributed System
	Model Checking
	Formal Verification
DCTERMS.abstract	モデル検査など形式モデルに基づくソフトウェアシステムの形式的検証は高い信頼性を持つソフトウェアの構築を可能にすると期待されている.さらに,分散システムにおいてはネットワーク上の遅延,遅延変動(ジッタ),帯域幅,パケットロスパラメータなどを管理して,要求されるQoSを達成することが重要とされる.そこで,本研究では確率的振る舞いを持つシステムに対するモデル検査ツールPRISMに着目し,これを用いたリアルタイムマルチメディアシステムのネットワーク遅延を考慮した形式的検証手法を提案する.また本論文では,提案手法の有用性を明らかにするために例題に適用し,その評価と考察についても述べる.
DCTERMS.abstract	Formal verification techniques, especially model checking techniques are promising techniques in software developing due to their ability of exhaustive checking. For distributed systems, managing QoS parameters, such as latency, network delay, jitters, bandwidth and packet loss, is a focal point of their quality. In this paper, focusing using PRISM, a model checker for probabilistic real-time systems, we present a new method to analysis real-time multi-media systems considering network properties. The paper also describes an application example and the result.
DC.rights	Copyright © 2006 IEICE
DC.rights	本文データはCiNiiから複製したものである
DC.format	27429
citation_title	確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について
citation_author	長井, 栄吾
	岡野, 浩三
	楠本, 真二
citation_publisher	電子情報通信学会
citation_language	日本語
citation_date	2006-01-27
citation_journal_title	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
citation_volume	105
citation_issue	597
citation_firstpage	19
citation_lastpage	24
citation_public_url	https://hdl.handle.net/11094/27429

確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について

閲覧可能ファイル

論文情報

論文詳細を表示