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

摘要

モデル検査など形式モデルに基づくソフトウェアシステムの形式的検証は高い侶瓶性を持つソフトウェアの構築を可能にすると期待されている, さらに∫分散システムにかてはネットワーク上の遅延，遅延変動（ジッタ），帯域帽，パケットロスパラメータなどを管理して，要求されるqo5を速成することが重要とされる. そこで, 本研究では確率的振る舞いを持つシステムに対するモデル検査ソールPRISMに着，これを用いたリアルタイムマルチメディアシステムのネットワーク遅延を考乱た形式的検証手法を曙案する．また本論文では, 提案手法の有月順を明らかにするために例題に適用し，その評価と考察についても述べる．