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

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

このアイテムのアクセス数:107件（2022-05-17 04:22 集計）

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

閲覧可能ファイル

ファイル	フォーマット	サイズ	閲覧回数	説明
itr105_597_019	pdf	687 KB	89

論文情報

タイトル	確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について
別タイトル	A Verification Considering the Network Delay for Real-time Distributed Systems with the Probabilistic Model Checker PRISM
タイトル (ヨミ)	カクリツテキ　モデル　ケンサ　ツール　PRISM　ニ　ヨル　リアルタイム　ブンサン　システム　ノ　ネットワーク　チエン　ヲ　コウリョ　シタ　ケンショウ　シュホウ　ニ　ツイテ
著者	長井, 栄吾長井, 栄吾
	岡野, 浩三岡野, 浩三
	楠本, 真二楠本, 真二
著者の別表記	Nagai, Eigo
	Okano, Kozo
	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
ISSN	09135685
NCID	AN10013287
URL	http://hdl.handle.net/11094/27429
権利情報	Copyright © 2006 IEICE
権利情報	本文データはCiNiiから複製したものである
言語	日本語
カテゴリ	学術雑誌論文 Journal Article

著者版フラグ	publisher
NII資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
dcmi資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス.105(597) P.19-P.24
DC.title	確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について
DCTERMS.alternative	A Verification Considering the Network Delay for Real-time Distributed Systems with the Probabilistic Model Checker PRISM
DC.creator	長井, 栄吾
	岡野, 浩三
	楠本, 真二
DC.creator	Nagai, Eigo
	Okano, Kozo
	Kusumoto, Shinji
DC.publisher	電子情報通信学会
DC.language" scheme="DCTERMS.RFC1766	日本語
DCTERMS.issued" scheme="DCTERMS.W3CDTF	2006-01-27
DC.identifier" scheme="DCTERMS.URI	http://hdl.handle.net/11094/27429
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から複製したものである
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_issn	09135685
citation_public_url	http://hdl.handle.net/11094/27429
citation_keywords	リアルタイム分散システム
	モデル検査
	PRISM
	形式的検証
	Real-time Distributed System
	Model Checking
	Formal Verification

閲覧可能ファイル

論文情報

論文詳細を表示