QoS Analysis of Real-Time Distributed Systems Based on Hybrid Analysis of Probabilistic Model Checking Technique and Simulation

Takeshi NAGAOKA  Akihiko ITO  Kozo OKANO  Shinji KUSUMOTO  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E94-D   No.5   pp.958-966
Publication Date: 2011/05/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.E94.D.958
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Model Checking
Keyword: 
QoS,  probabilistic automaton,  simulation,  model checking,  

Full Text: PDF>>
Buy this Article




Summary: 
For the Internet, system developers often have to estimate the QoS by simulation techniques or mathematical analysis. Probabilistic model checking can evaluate performance, dependability and stability of information processing systems with random behaviors. We apply a hybrid analysis approach onto real-time distributed systems. In the hybrid analysis approach, we perform stepwise analysis using probabilistic models of target systems in different abstract levels. First, we create a probabilistic model with detailed behavior of the system (called detailed model), and apply simulation on the detailed model. Next, based on the simulation results, we create a probabilistic model in an abstract level (called simplified model). Then, we verify qualitative properties using the probabilistic model checking techniques. This prevents from state-explosion. We evaluate the validity of our approach by comparing to simulation results of NS-2 using a case study of a video data streaming system. The experiments show that the result of the proposed approach is very close to that of NS-2 simulation. The result encourages the approach is useful for the performance analysis on various domain.