A Probabilistic QoS Model-Checking for Dynamic Routing Protocol

Dynamic routing protocol involves the purchase order management among six participants which cooperate by multiple service interactions. Due to the complexities of interactions, it is important to check if the protocol will be stuck due to the fact that some required channels are not available (i.e. channel-absence) when an interaction is executed. Moreover, the quality of service (QoS) of the protocol is also important to decide the success of the purchase order business. In order to model checking the functional and non-functional properties of this protocol, this paper uses Web service choreography language Chor_r to describe the protocol. Since Chor_r is annotated with execution rate for each interaction, we can translate Chor_r into the input language of the probabilistic model checker PRISM for stochastic analysis of the protocol.