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

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

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

Number of Access:527（2025-09-04 14:41 Counts）

Identifier to cite or link to this item: https://hdl.handle.net/11094/27429

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
itr105_597_019 pdf None 687 KB 133 2014.04.11  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について
A Verification Considering the Network Delay for Real-time Distributed Systems with the Probabilistic Model Checker PRISM
カクリツテキ　モデル　ケンサ　ツール　PRISM　ニ　ヨル　リアルタイム　ブンサン　システム　ノ　ネットワーク　チエン　ヲ　コウリョ　シタ　ケンショウ　シュホウ　ニ　ツイテ
Creator
CreatorName
長井, 栄吾 ; ナガイ, エイゴ ; Nagai, Eigo
NRID
1000070252632 1000070252632
CreatorName
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000030234438 1000030234438
researchmap permalink
read0013799 read0013799
Scopus Author ID
7102741360 7102741360
CreatorName
楠本, 真二 ; クスモト, シンジ ; Kusumoto, Shinji
Subject
リアルタイム分散システム
モデル検査
PRISM
形式的検証
Real-time Distributed System
Model Checking
Formal Verification
Abstract
モデル検査など形式モデルに基づくソフトウェアシステムの形式的検証は高い信頼性を持つソフトウェアの構築を可能にすると期待されている.さらに,分散システムにおいてはネットワーク上の遅延,遅延変動(ジッタ),帯域幅,パケットロスパラメータなどを管理して,要求される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.
Publisher
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
Source Title
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
Volume (Issue)
105(597)
Page
19-24
Date of Issued
2006-01-27
Language
Japanese
Handle URL
https://hdl.handle.net/11094/27429
PISSN
09135685
NCID
AN10013287
Access Rights
open access
CopyRight
Copyright © 2006 IEICE
本文データはCiNiiから複製したものである
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article