Quantitative Verification of Navigation Model for Reliable Web Applications

Due to the stochastic nature and time constrains, it is important to quantitatively verify the reliability of Web applications as well as the usability. However, the reliability involves different kinds of QoS metrics, which is hard to be verified by the "yes" or "no" assertion in general model checking. This paper proposes a verification approach to analyzing the performance of the navigation model for reliable Web applications, aiming at verifying probabilistic timed specifications in a quantitative way. First, in order to investigate the time constrains and probabilistic behaviors, probabilistic timed automata (PTA) is introduced to improve the on-the-fly navigation model. Then, this work distinguishes the normal states and error states of BLM for assessing the capability of faults detection. Moreover, the discrete transition error locations and time transition error locations are discussed, which are used to evaluate the capability of fault tolerance. Third, to quantitatively verify the reliability properties, Probabilistic Timed Computation Tree Logic (PTCTL) formulae are employed to express the capability of faults detection and fault tolerance, and the probabilistic model checker PRISM is used to perform verification and output the quantitative results. For illustration, a simple audit system of a Web application is exemplified.